src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
author blanchet
Thu, 16 Dec 2010 15:12:17 +0100
changeset 41205 209546e0af2c
parent 41204 bd57cf5944cb
child 41207 f9c7bdc75dd0
permissions -rw-r--r--
comment tuning
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
38988
483879af0643 finished renaming
blanchet
parents: 38986
diff changeset
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_filter.ML
38027
505657ddb047 standardize "Author" tags
blanchet
parents: 37995
diff changeset
     2
    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
36393
be73a2b2443b support readable names even when Isar proof reconstruction is enabled -- useful for debugging
blanchet
parents: 36227
diff changeset
     3
    Author:     Jasmin Blanchette, TU Muenchen
39958
88c9aa5666de tuned comments
blanchet
parents: 39946
diff changeset
     4
88c9aa5666de tuned comments
blanchet
parents: 39946
diff changeset
     5
Sledgehammer's relevance filter.
33309
5f67433e6dd8 proper header;
wenzelm
parents: 33306
diff changeset
     6
*)
15452
e2a721567f67 Jia Meng: delta simpsets and clasets
paulson
parents: 15347
diff changeset
     7
38988
483879af0643 finished renaming
blanchet
parents: 38986
diff changeset
     8
signature SLEDGEHAMMER_FILTER =
16802
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
     9
sig
38993
504b9e1efd33 give priority to assumptions in structured proofs
blanchet
parents: 38992
diff changeset
    10
  datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
    11
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    12
  type relevance_fudge =
41159
1e12d6495423 honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents: 41158
diff changeset
    13
    {allow_ext : bool,
1e12d6495423 honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents: 41158
diff changeset
    14
     worse_irrel_freq : real,
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    15
     higher_order_irrel_weight : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    16
     abs_rel_weight : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    17
     abs_irrel_weight : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    18
     skolem_irrel_weight : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    19
     theory_const_rel_weight : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    20
     theory_const_irrel_weight : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    21
     intro_bonus : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    22
     elim_bonus : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    23
     simp_bonus : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    24
     local_bonus : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    25
     assum_bonus : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    26
     chained_bonus : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    27
     max_imperfect : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    28
     max_imperfect_exp : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    29
     threshold_divisor : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    30
     ridiculous_threshold : real}
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    31
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35963
diff changeset
    32
  type relevance_override =
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    33
    {add : (Facts.ref * Attrib.src list) list,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    34
     del : (Facts.ref * Attrib.src list) list,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    35
     only : bool}
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35963
diff changeset
    36
37616
c8d2d84d6011 always perform relevance filtering on original formulas
blanchet
parents: 37580
diff changeset
    37
  val trace : bool Unsynchronized.ref
40205
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
    38
  val fact_from_ref :
38996
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
    39
    Proof.context -> unit Symtab.table -> thm list
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
    40
    -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
37347
635425a442e8 show more respect for user-specified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents: 37345
diff changeset
    41
  val relevant_facts :
41066
3890ef4e02f9 pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
blanchet
parents: 40418
diff changeset
    42
    Proof.context -> bool -> real * real -> int
3890ef4e02f9 pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
blanchet
parents: 40418
diff changeset
    43
    -> (string * typ -> term list -> bool) -> relevance_fudge
3890ef4e02f9 pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
blanchet
parents: 40418
diff changeset
    44
    -> relevance_override -> thm list -> term list -> term
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    45
    -> ((string * locality) * thm) list
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    46
end;
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    47
38988
483879af0643 finished renaming
blanchet
parents: 38986
diff changeset
    48
structure Sledgehammer_Filter : SLEDGEHAMMER_FILTER =
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    49
struct
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    50
38652
e063be321438 perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents: 38644
diff changeset
    51
open Sledgehammer_Util
e063be321438 perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents: 38644
diff changeset
    52
37616
c8d2d84d6011 always perform relevance filtering on original formulas
blanchet
parents: 37580
diff changeset
    53
val trace = Unsynchronized.ref false
c8d2d84d6011 always perform relevance filtering on original formulas
blanchet
parents: 37580
diff changeset
    54
fun trace_msg msg = if !trace then tracing (msg ()) else ()
35826
1590abc3d42a renamed Sledgehammer structures
blanchet
parents: 35825
diff changeset
    55
41204
bd57cf5944cb get rid of experimental feature of term patterns in relevance filter -- doesn't work well unless we take into consideration the equality theory entailed by the relevant facts
blanchet
parents: 41202
diff changeset
    56
(* experimental feature *)
38997
78ac4468cf9d got rid of the "theory_relevant" option;
blanchet
parents: 38996
diff changeset
    57
val respect_no_atp = true
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
    58
38993
504b9e1efd33 give priority to assumptions in structured proofs
blanchet
parents: 38992
diff changeset
    59
datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
    60
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    61
type relevance_fudge =
41159
1e12d6495423 honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents: 41158
diff changeset
    62
  {allow_ext : bool,
1e12d6495423 honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents: 41158
diff changeset
    63
   worse_irrel_freq : real,
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    64
   higher_order_irrel_weight : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    65
   abs_rel_weight : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    66
   abs_irrel_weight : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    67
   skolem_irrel_weight : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    68
   theory_const_rel_weight : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    69
   theory_const_irrel_weight : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    70
   intro_bonus : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    71
   elim_bonus : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    72
   simp_bonus : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    73
   local_bonus : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    74
   assum_bonus : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    75
   chained_bonus : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    76
   max_imperfect : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    77
   max_imperfect_exp : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    78
   threshold_divisor : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    79
   ridiculous_threshold : real}
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    80
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35963
diff changeset
    81
type relevance_override =
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    82
  {add : (Facts.ref * Attrib.src list) list,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    83
   del : (Facts.ref * Attrib.src list) list,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    84
   only : bool}
21070
0a898140fea2 Added more debugging info
paulson
parents: 20995
diff changeset
    85
37616
c8d2d84d6011 always perform relevance filtering on original formulas
blanchet
parents: 37580
diff changeset
    86
val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
39896
13b3a2ba9ea7 encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents: 39718
diff changeset
    87
val abs_name = sledgehammer_prefix ^ "abs"
13b3a2ba9ea7 encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents: 39718
diff changeset
    88
val skolem_prefix = sledgehammer_prefix ^ "sko"
38992
542474156c66 introduce fudge factors to deal with "theory const"
blanchet
parents: 38988
diff changeset
    89
val theory_const_suffix = Long_Name.separator ^ " 1"
37616
c8d2d84d6011 always perform relevance filtering on original formulas
blanchet
parents: 37580
diff changeset
    90
40227
e31e3f0071d4 support non-identifier-like fact names in Sledgehammer (e.g., "my lemma") by quoting them
blanchet
parents: 40205
diff changeset
    91
fun needs_quoting reserved s =
40375
db690d38e4b9 fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents: 40373
diff changeset
    92
  Symtab.defined reserved s orelse
db690d38e4b9 fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents: 40373
diff changeset
    93
  exists (not o Syntax.is_identifier) (Long_Name.explode s)
40227
e31e3f0071d4 support non-identifier-like fact names in Sledgehammer (e.g., "my lemma") by quoting them
blanchet
parents: 40205
diff changeset
    94
40375
db690d38e4b9 fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents: 40373
diff changeset
    95
fun make_name reserved multi j name =
40227
e31e3f0071d4 support non-identifier-like fact names in Sledgehammer (e.g., "my lemma") by quoting them
blanchet
parents: 40205
diff changeset
    96
  (name |> needs_quoting reserved name ? quote) ^
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
    97
  (if multi then "(" ^ Int.toString j ^ ")" else "")
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
    98
40375
db690d38e4b9 fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents: 40373
diff changeset
    99
fun explode_interval _ (Facts.FromTo (i, j)) = i upto j
db690d38e4b9 fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents: 40373
diff changeset
   100
  | explode_interval max (Facts.From i) = i upto i + max - 1
db690d38e4b9 fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents: 40373
diff changeset
   101
  | explode_interval _ (Facts.Single i) = [i]
db690d38e4b9 fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents: 40373
diff changeset
   102
40205
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   103
fun fact_from_ref ctxt reserved chained_ths (xthm as (xref, args)) =
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   104
  let
38996
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
   105
    val ths = Attrib.eval_thms ctxt [xthm]
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
   106
    val bracket =
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
   107
      implode (map (fn arg => "[" ^ Pretty.str_of (Args.pretty_src ctxt arg)
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
   108
                               ^ "]") args)
40375
db690d38e4b9 fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents: 40373
diff changeset
   109
    fun nth_name j =
38996
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
   110
      case xref of
39264
blanchet
parents: 39012
diff changeset
   111
        Facts.Fact s => "`" ^ s ^ "`" ^ bracket
38996
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
   112
      | Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
40375
db690d38e4b9 fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents: 40373
diff changeset
   113
      | Facts.Named ((name, _), NONE) =>
db690d38e4b9 fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents: 40373
diff changeset
   114
        make_name reserved (length ths > 1) (j + 1) name ^ bracket
db690d38e4b9 fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents: 40373
diff changeset
   115
      | Facts.Named ((name, _), SOME intervals) =>
db690d38e4b9 fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents: 40373
diff changeset
   116
        make_name reserved true
db690d38e4b9 fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents: 40373
diff changeset
   117
                 (nth (maps (explode_interval (length ths)) intervals) j) name ^
db690d38e4b9 fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents: 40373
diff changeset
   118
        bracket
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   119
  in
40375
db690d38e4b9 fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents: 40373
diff changeset
   120
    (ths, (0, []))
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   121
    |-> fold (fn th => fn (j, rest) =>
40375
db690d38e4b9 fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents: 40373
diff changeset
   122
                 (j + 1, ((nth_name j,
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   123
                          if member Thm.eq_thm chained_ths th then Chained
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   124
                          else General), th) :: rest))
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   125
    |> snd
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   126
  end
37616
c8d2d84d6011 always perform relevance filtering on original formulas
blanchet
parents: 37580
diff changeset
   127
41199
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   128
(* This is a terrible hack. Free variables are sometimes code as "M__" when they
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   129
   are displayed as "M" and we want to avoid clashes with these. But sometimes
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   130
   it's even worse: "Ma__" encodes "M". So we simply reserve all prefixes of all
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   131
   free variables. In the worse case scenario, where the fact won't be resolved
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   132
   correctly, the user can fix it manually, e.g., by naming the fact in
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   133
   question. Ideally we would need nothing of it, but backticks just don't work
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   134
   with schematic variables. *)
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   135
fun all_prefixes_of s =
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   136
  map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   137
fun close_form t =
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   138
  (t, [] |> Term.add_free_names t |> maps all_prefixes_of)
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   139
  |> fold (fn ((s, i), T) => fn (t', taken) =>
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   140
              let val s' = Name.variant taken s in
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   141
                ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   142
                  else Term.all) T
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   143
                 $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   144
                 s' :: taken)
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   145
              end)
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   146
          (Term.add_vars t [] |> sort_wrt (fst o fst))
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   147
  |> fst
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   148
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   149
fun string_for_term ctxt t =
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   150
  Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   151
                   (print_mode_value ())) (Syntax.string_of_term ctxt) t
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   152
  |> String.translate (fn c => if Char.isPrint c then str c else "")
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   153
  |> simplify_spaces
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   154
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   155
(** Structural induction rules **)
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   156
41200
6cc9b6fd7f6f add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents: 41199
diff changeset
   157
fun struct_induct_rule_on th =
41199
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   158
  case Logic.strip_horn (prop_of th) of
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   159
    (prems, @{const Trueprop}
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   160
            $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   161
    if not (is_TVar ind_T) andalso length prems > 1 andalso
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   162
       exists (exists_subterm (curry (op aconv) p)) prems andalso
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   163
       not (exists (exists_subterm (curry (op aconv) a)) prems) then
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   164
      SOME (p_name, ind_T)
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   165
    else
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   166
      NONE
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   167
  | _ => NONE
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   168
41202
bf00e0a578e8 make it more likely that induction rules are picked up by Sledgehammer
blanchet
parents: 41200
diff changeset
   169
fun instantiate_induct_rule ctxt concl_prop p_name ((name, _), (multi, th))
41199
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   170
                            ind_x =
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   171
  let
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   172
    fun varify_noninducts (t as Free (s, T)) =
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   173
        if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   174
      | varify_noninducts t = t
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   175
    val p_inst =
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   176
      concl_prop |> map_aterms varify_noninducts |> close_form
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   177
                 |> lambda (Free ind_x)
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   178
                 |> string_for_term ctxt
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   179
  in
41202
bf00e0a578e8 make it more likely that induction rules are picked up by Sledgehammer
blanchet
parents: 41200
diff changeset
   180
    ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
bf00e0a578e8 make it more likely that induction rules are picked up by Sledgehammer
blanchet
parents: 41200
diff changeset
   181
      Local),
41199
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   182
     (multi, th |> read_instantiate ctxt [((p_name, 0), p_inst)]))
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   183
  end
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   184
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   185
fun type_match thy (T1, T2) =
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   186
  (Sign.typ_match thy (T2, T1) Vartab.empty; true)
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   187
  handle Type.TYPE_MATCH => false
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   188
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   189
fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, (_, th))) =
41200
6cc9b6fd7f6f add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents: 41199
diff changeset
   190
  case struct_induct_rule_on th of
41199
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   191
    SOME (p_name, ind_T) =>
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   192
    let val thy = ProofContext.theory_of ctxt in
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   193
      stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T))
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   194
              |> map_filter (try (instantiate_induct_rule ctxt stmt p_name ax))
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   195
    end
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   196
  | NONE => [ax]
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   197
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents: 28065
diff changeset
   198
(***************************************************************)
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents: 28065
diff changeset
   199
(* Relevance Filtering                                         *)
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents: 28065
diff changeset
   200
(***************************************************************)
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   201
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   202
(*** constants with types ***)
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   203
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   204
fun order_of_type (Type (@{type_name fun}, [T1, @{typ bool}])) =
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   205
    order_of_type T1 (* cheat: pretend sets are first-order *)
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   206
  | order_of_type (Type (@{type_name fun}, [T1, T2])) =
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   207
    Int.max (order_of_type T1 + 1, order_of_type T2)
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   208
  | order_of_type (Type (_, Ts)) = fold (Integer.max o order_of_type) Ts 0
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   209
  | order_of_type _ = 0
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   210
38823
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   211
(* An abstraction of Isabelle types and first-order terms *)
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   212
datatype pattern = PVar | PApp of string * pattern list
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   213
datatype ptype = PType of int * pattern list
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   214
38823
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   215
fun string_for_pattern PVar = "_"
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   216
  | string_for_pattern (PApp (s, ps)) =
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   217
    if null ps then s else s ^ string_for_patterns ps
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   218
and string_for_patterns ps = "(" ^ commas (map string_for_pattern ps) ^ ")"
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   219
fun string_for_ptype (PType (_, ps)) = string_for_patterns ps
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   220
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   221
(*Is the second type an instance of the first one?*)
38824
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
   222
fun match_pattern (PVar, _) = true
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
   223
  | match_pattern (PApp _, PVar) = false
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
   224
  | match_pattern (PApp (s, ps), PApp (t, qs)) =
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
   225
    s = t andalso match_patterns (ps, qs)
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
   226
and match_patterns (_, []) = true
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
   227
  | match_patterns ([], _) = false
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
   228
  | match_patterns (p :: ps, q :: qs) =
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
   229
    match_pattern (p, q) andalso match_patterns (ps, qs)
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   230
fun match_ptype (PType (_, ps), PType (_, qs)) = match_patterns (ps, qs)
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   231
38823
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   232
(* Is there a unifiable constant? *)
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   233
fun pconst_mem f consts (s, ps) =
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   234
  exists (curry (match_ptype o f) ps)
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   235
         (map snd (filter (curry (op =) s o fst) consts))
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   236
fun pconst_hyper_mem f const_tab (s, ps) =
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   237
  exists (curry (match_ptype o f) ps) (these (Symtab.lookup const_tab s))
37505
d9af5c01dc4a added code to optionally perform fact filtering on the original (non-CNF) formulas
blanchet
parents: 37504
diff changeset
   238
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   239
fun pattern_for_type (Type (s, Ts)) = PApp (s, map pattern_for_type Ts)
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   240
  | pattern_for_type (TFree (s, _)) = PApp (s, [])
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   241
  | pattern_for_type (TVar _) = PVar
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   242
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   243
(* Pairs a constant with the list of its type instantiations. *)
41204
bd57cf5944cb get rid of experimental feature of term patterns in relevance filter -- doesn't work well unless we take into consideration the equality theory entailed by the relevant facts
blanchet
parents: 41202
diff changeset
   244
fun ptype thy const x =
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   245
  (if const then map pattern_for_type (these (try (Sign.const_typargs thy) x))
41204
bd57cf5944cb get rid of experimental feature of term patterns in relevance filter -- doesn't work well unless we take into consideration the equality theory entailed by the relevant facts
blanchet
parents: 41202
diff changeset
   246
   else [])
bd57cf5944cb get rid of experimental feature of term patterns in relevance filter -- doesn't work well unless we take into consideration the equality theory entailed by the relevant facts
blanchet
parents: 41202
diff changeset
   247
fun rich_ptype thy const (s, T) =
bd57cf5944cb get rid of experimental feature of term patterns in relevance filter -- doesn't work well unless we take into consideration the equality theory entailed by the relevant facts
blanchet
parents: 41202
diff changeset
   248
  PType (order_of_type T, ptype thy const (s, T))
bd57cf5944cb get rid of experimental feature of term patterns in relevance filter -- doesn't work well unless we take into consideration the equality theory entailed by the relevant facts
blanchet
parents: 41202
diff changeset
   249
fun rich_pconst thy const (s, T) = (s, rich_ptype thy const (s, T))
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   250
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   251
fun string_for_hyper_pconst (s, ps) =
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   252
  s ^ "{" ^ commas (map string_for_ptype ps) ^ "}"
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   253
38823
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   254
(* Add a pconstant to the table, but a [] entry means a standard
38819
71c9f61516cd if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents: 38818
diff changeset
   255
   connective, which we ignore.*)
41066
3890ef4e02f9 pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
blanchet
parents: 40418
diff changeset
   256
fun add_pconst_to_table also_skolem (s, p) =
3890ef4e02f9 pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
blanchet
parents: 40418
diff changeset
   257
  if (not also_skolem andalso String.isPrefix skolem_prefix s) then I
3890ef4e02f9 pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
blanchet
parents: 40418
diff changeset
   258
  else Symtab.map_default (s, [p]) (insert (op =) p)
38819
71c9f61516cd if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents: 38818
diff changeset
   259
71c9f61516cd if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents: 38818
diff changeset
   260
fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
71c9f61516cd if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents: 38818
diff changeset
   261
40369
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40251
diff changeset
   262
fun pconsts_in_terms thy is_built_in_const also_skolems pos ts =
37505
d9af5c01dc4a added code to optionally perform fact filtering on the original (non-CNF) formulas
blanchet
parents: 37504
diff changeset
   263
  let
41202
bf00e0a578e8 make it more likely that induction rules are picked up by Sledgehammer
blanchet
parents: 41200
diff changeset
   264
    (* Giving a penalty to Skolems is a good idea, but that penalty shouldn't
bf00e0a578e8 make it more likely that induction rules are picked up by Sledgehammer
blanchet
parents: 41200
diff changeset
   265
       increase linearly with the number of Skolems in the fact. Hence, we
bf00e0a578e8 make it more likely that induction rules are picked up by Sledgehammer
blanchet
parents: 41200
diff changeset
   266
       create equivalence classes of Skolems by reusing fresh Skolem names. *)
bf00e0a578e8 make it more likely that induction rules are picked up by Sledgehammer
blanchet
parents: 41200
diff changeset
   267
    val skolem_cache = Unsynchronized.ref ""
bf00e0a578e8 make it more likely that induction rules are picked up by Sledgehammer
blanchet
parents: 41200
diff changeset
   268
    fun get_skolem_name () =
bf00e0a578e8 make it more likely that induction rules are picked up by Sledgehammer
blanchet
parents: 41200
diff changeset
   269
      (if !skolem_cache = "" then skolem_cache := gensym skolem_prefix else ();
bf00e0a578e8 make it more likely that induction rules are picked up by Sledgehammer
blanchet
parents: 41200
diff changeset
   270
       !skolem_cache)
38819
71c9f61516cd if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents: 38818
diff changeset
   271
    val flip = Option.map not
38587
1317657d6aa9 fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents: 38395
diff changeset
   272
    (* We include free variables, as well as constants, to handle locales. For
41205
209546e0af2c comment tuning
blanchet
parents: 41204
diff changeset
   273
       each quantifiers that must necessarily be skolemized by the automatic
209546e0af2c comment tuning
blanchet
parents: 41204
diff changeset
   274
       prover, we introduce a fresh constant to simulate the effect of
209546e0af2c comment tuning
blanchet
parents: 41204
diff changeset
   275
       Skolemization. *)
40373
ff0e17a9d840 pass proper type to SMT_Builtin.is_builtin
blanchet
parents: 40371
diff changeset
   276
    fun do_const const x ts =
41066
3890ef4e02f9 pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
blanchet
parents: 40418
diff changeset
   277
      (not (is_built_in_const x ts)
41204
bd57cf5944cb get rid of experimental feature of term patterns in relevance filter -- doesn't work well unless we take into consideration the equality theory entailed by the relevant facts
blanchet
parents: 41202
diff changeset
   278
       ? add_pconst_to_table also_skolems (rich_pconst thy const x))
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   279
      #> fold do_term ts
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   280
    and do_term t =
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   281
      case strip_comb t of
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   282
        (Const x, ts) => do_const true x ts
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   283
      | (Free x, ts) => do_const false x ts
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   284
      | (Abs (_, T, t'), ts) =>
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   285
        (null ts
41066
3890ef4e02f9 pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
blanchet
parents: 40418
diff changeset
   286
         ? add_pconst_to_table true (abs_name, PType (order_of_type T + 1, [])))
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   287
        #> fold do_term (t' :: ts)
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   288
      | (_, ts) => fold do_term ts
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   289
    fun do_quantifier will_surely_be_skolemized abs_T body_t =
37537
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   290
      do_formula pos body_t
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   291
      #> (if also_skolems andalso will_surely_be_skolemized then
41066
3890ef4e02f9 pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
blanchet
parents: 40418
diff changeset
   292
            add_pconst_to_table true
41202
bf00e0a578e8 make it more likely that induction rules are picked up by Sledgehammer
blanchet
parents: 41200
diff changeset
   293
                (get_skolem_name (), PType (order_of_type abs_T, []))
38587
1317657d6aa9 fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents: 38395
diff changeset
   294
          else
1317657d6aa9 fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents: 38395
diff changeset
   295
            I)
1317657d6aa9 fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents: 38395
diff changeset
   296
    and do_term_or_formula T =
38692
89d3550d8e16 cosmetics
blanchet
parents: 38689
diff changeset
   297
      if is_formula_type T then do_formula NONE else do_term
37537
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   298
    and do_formula pos t =
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   299
      case t of
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   300
        Const (@{const_name all}, _) $ Abs (_, T, t') =>
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   301
        do_quantifier (pos = SOME false) T t'
37537
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   302
      | @{const "==>"} $ t1 $ t2 =>
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   303
        do_formula (flip pos) t1 #> do_formula pos t2
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   304
      | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
38587
1317657d6aa9 fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents: 38395
diff changeset
   305
        fold (do_term_or_formula T) [t1, t2]
37537
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   306
      | @{const Trueprop} $ t1 => do_formula pos t1
41140
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   307
      | @{const False} => I
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   308
      | @{const True} => I
37537
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   309
      | @{const Not} $ t1 => do_formula (flip pos) t1
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   310
      | Const (@{const_name All}, _) $ Abs (_, T, t') =>
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   311
        do_quantifier (pos = SOME false) T t'
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   312
      | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   313
        do_quantifier (pos = SOME true) T t'
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   314
      | @{const HOL.conj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   315
      | @{const HOL.disj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
38786
e46e7a9cb622 formerly unnamed infix impliciation now named HOL.implies
haftmann
parents: 38752
diff changeset
   316
      | @{const HOL.implies} $ t1 $ t2 =>
37537
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   317
        do_formula (flip pos) t1 #> do_formula pos t2
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38829
diff changeset
   318
      | Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2 =>
38587
1317657d6aa9 fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents: 38395
diff changeset
   319
        fold (do_term_or_formula T) [t1, t2]
1317657d6aa9 fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents: 38395
diff changeset
   320
      | Const (@{const_name If}, Type (_, [_, Type (_, [T, _])]))
1317657d6aa9 fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents: 38395
diff changeset
   321
        $ t1 $ t2 $ t3 =>
1317657d6aa9 fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents: 38395
diff changeset
   322
        do_formula NONE t1 #> fold (do_term_or_formula T) [t2, t3]
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   323
      | Const (@{const_name Ex1}, _) $ Abs (_, T, t') =>
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   324
        do_quantifier (is_some pos) T t'
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   325
      | Const (@{const_name Ball}, _) $ t1 $ Abs (_, T, t') =>
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   326
        do_quantifier (pos = SOME false) T
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   327
                      (HOLogic.mk_imp (incr_boundvars 1 t1 $ Bound 0, t'))
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   328
      | Const (@{const_name Bex}, _) $ t1 $ Abs (_, T, t') =>
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   329
        do_quantifier (pos = SOME true) T
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   330
                      (HOLogic.mk_conj (incr_boundvars 1 t1 $ Bound 0, t'))
37537
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   331
      | (t0 as Const (_, @{typ bool})) $ t1 =>
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   332
        do_term t0 #> do_formula pos t1  (* theory constant *)
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   333
      | _ => do_term t
38819
71c9f61516cd if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents: 38818
diff changeset
   334
  in Symtab.empty |> fold (do_formula pos) ts end
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   335
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   336
(*Inserts a dummy "constant" referring to the theory name, so that relevance
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   337
  takes the given theory into account.*)
41200
6cc9b6fd7f6f add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents: 41199
diff changeset
   338
fun theory_constify ({theory_const_rel_weight, theory_const_irrel_weight, ...}
6cc9b6fd7f6f add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents: 41199
diff changeset
   339
                     : relevance_fudge) thy_name t =
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   340
  if exists (curry (op <) 0.0) [theory_const_rel_weight,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   341
                                theory_const_irrel_weight] then
41200
6cc9b6fd7f6f add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents: 41199
diff changeset
   342
    Const (thy_name ^ theory_const_suffix, @{typ bool}) $ t
37505
d9af5c01dc4a added code to optionally perform fact filtering on the original (non-CNF) formulas
blanchet
parents: 37504
diff changeset
   343
  else
41200
6cc9b6fd7f6f add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents: 41199
diff changeset
   344
    t
6cc9b6fd7f6f add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents: 41199
diff changeset
   345
6cc9b6fd7f6f add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents: 41199
diff changeset
   346
fun theory_const_prop_of fudge th =
6cc9b6fd7f6f add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents: 41199
diff changeset
   347
  theory_constify fudge (Context.theory_name (theory_of_thm th)) (prop_of th)
37505
d9af5c01dc4a added code to optionally perform fact filtering on the original (non-CNF) formulas
blanchet
parents: 37504
diff changeset
   348
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   349
(**** Constant / Type Frequencies ****)
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   350
38743
69fa75354c58 simplify more code
blanchet
parents: 38742
diff changeset
   351
(* A two-dimensional symbol table counts frequencies of constants. It's keyed
69fa75354c58 simplify more code
blanchet
parents: 38742
diff changeset
   352
   first by constant name and second by its list of type instantiations. For the
38823
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   353
   latter, we need a linear ordering on "pattern list". *)
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   354
38823
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   355
fun pattern_ord p =
38743
69fa75354c58 simplify more code
blanchet
parents: 38742
diff changeset
   356
  case p of
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   357
    (PVar, PVar) => EQUAL
38823
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   358
  | (PVar, PApp _) => LESS
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   359
  | (PApp _, PVar) => GREATER
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   360
  | (PApp q1, PApp q2) =>
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   361
    prod_ord fast_string_ord (dict_ord pattern_ord) (q1, q2)
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   362
fun ptype_ord (PType p, PType q) =
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   363
  prod_ord (dict_ord pattern_ord) int_ord (swap p, swap q)
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   364
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   365
structure PType_Tab = Table(type key = ptype val ord = ptype_ord)
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   366
40204
da97d75e20e6 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents: 40191
diff changeset
   367
fun count_fact_consts thy fudge =
37503
c2dfa26b9da6 cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents: 37502
diff changeset
   368
  let
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   369
    fun do_const const (s, T) ts =
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   370
      (* Two-dimensional table update. Constant maps to types maps to count. *)
41204
bd57cf5944cb get rid of experimental feature of term patterns in relevance filter -- doesn't work well unless we take into consideration the equality theory entailed by the relevant facts
blanchet
parents: 41202
diff changeset
   371
      PType_Tab.map_default (rich_ptype thy const (s, T), 0) (Integer.add 1)
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   372
      |> Symtab.map_default (s, PType_Tab.empty)
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   373
      #> fold do_term ts
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   374
    and do_term t =
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   375
      case strip_comb t of
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   376
        (Const x, ts) => do_const true x ts
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   377
      | (Free x, ts) => do_const false x ts
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   378
      | (Abs (_, _, t'), ts) => fold do_term (t' :: ts)
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   379
      | (_, ts) => fold do_term ts
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   380
  in do_term o theory_const_prop_of fudge o snd end
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   381
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   382
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   383
(**** Actual Filtering Code ****)
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   384
39367
blanchet
parents: 39366
diff changeset
   385
fun pow_int _ 0 = 1.0
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   386
  | pow_int x 1 = x
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   387
  | pow_int x n = if n > 0 then x * pow_int x (n - 1) else pow_int x (n + 1) / x
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   388
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   389
(*The frequency of a constant is the sum of those of all instances of its type.*)
38824
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
   390
fun pconst_freq match const_tab (c, ps) =
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   391
  PType_Tab.fold (fn (qs, m) => match (ps, qs) ? Integer.add m)
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   392
                 (the (Symtab.lookup const_tab c)) 0
38686
45eeee8d6b12 modified relevance filter
blanchet
parents: 38684
diff changeset
   393
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   394
38085
cc44e887246c avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents: 38027
diff changeset
   395
(* A surprising number of theorems contain only a few significant constants.
cc44e887246c avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents: 38027
diff changeset
   396
   These include all induction rules, and other general theorems. *)
37503
c2dfa26b9da6 cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents: 37502
diff changeset
   397
c2dfa26b9da6 cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents: 37502
diff changeset
   398
(* "log" seems best in practice. A constant function of one ignores the constant
38938
2b93dbc07778 improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents: 38937
diff changeset
   399
   frequencies. Rare constants give more points if they are relevant than less
2b93dbc07778 improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents: 38937
diff changeset
   400
   rare ones. *)
39367
blanchet
parents: 39366
diff changeset
   401
fun rel_weight_for _ freq = 1.0 + 2.0 / Math.ln (Real.fromInt freq + 1.0)
38938
2b93dbc07778 improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents: 38937
diff changeset
   402
2b93dbc07778 improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents: 38937
diff changeset
   403
(* Irrelevant constants are treated differently. We associate lower penalties to
2b93dbc07778 improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents: 38937
diff changeset
   404
   very rare constants and very common ones -- the former because they can't
2b93dbc07778 improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents: 38937
diff changeset
   405
   lead to the inclusion of too many new facts, and the latter because they are
2b93dbc07778 improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents: 38937
diff changeset
   406
   so common as to be of little interest. *)
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   407
fun irrel_weight_for ({worse_irrel_freq, higher_order_irrel_weight, ...}
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   408
                      : relevance_fudge) order freq =
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   409
  let val (k, x) = worse_irrel_freq |> `Real.ceil in
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   410
    (if freq < k then Math.ln (Real.fromInt (freq + 1)) / Math.ln x
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   411
     else rel_weight_for order freq / rel_weight_for order k)
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   412
    * pow_int higher_order_irrel_weight (order - 1)
38938
2b93dbc07778 improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents: 38937
diff changeset
   413
  end
37503
c2dfa26b9da6 cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents: 37502
diff changeset
   414
c2dfa26b9da6 cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents: 37502
diff changeset
   415
(* Computes a constant's weight, as determined by its frequency. *)
38992
542474156c66 introduce fudge factors to deal with "theory const"
blanchet
parents: 38988
diff changeset
   416
fun generic_pconst_weight abs_weight skolem_weight theory_const_weight
542474156c66 introduce fudge factors to deal with "theory const"
blanchet
parents: 38988
diff changeset
   417
                          weight_for f const_tab (c as (s, PType (m, _))) =
38816
21a6f261595e lower penalty for Skolem constants
blanchet
parents: 38752
diff changeset
   418
  if s = abs_name then abs_weight
21a6f261595e lower penalty for Skolem constants
blanchet
parents: 38752
diff changeset
   419
  else if String.isPrefix skolem_prefix s then skolem_weight
38992
542474156c66 introduce fudge factors to deal with "theory const"
blanchet
parents: 38988
diff changeset
   420
  else if String.isSuffix theory_const_suffix s then theory_const_weight
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   421
  else weight_for m (pconst_freq (match_ptype o f) const_tab c)
38821
d0275b6c4e9d avoid needless "that" fact
blanchet
parents: 38820
diff changeset
   422
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   423
fun rel_pconst_weight ({abs_rel_weight, theory_const_rel_weight, ...}
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   424
                       : relevance_fudge) const_tab =
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   425
  generic_pconst_weight abs_rel_weight 0.0 theory_const_rel_weight
38992
542474156c66 introduce fudge factors to deal with "theory const"
blanchet
parents: 38988
diff changeset
   426
                        rel_weight_for I const_tab
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   427
fun irrel_pconst_weight (fudge as {abs_irrel_weight, skolem_irrel_weight,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   428
                                   theory_const_irrel_weight, ...}) const_tab =
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   429
  generic_pconst_weight abs_irrel_weight skolem_irrel_weight
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   430
                        theory_const_irrel_weight (irrel_weight_for fudge) swap
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   431
                        const_tab
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   432
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   433
fun locality_bonus (_ : relevance_fudge) General = 0.0
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   434
  | locality_bonus {intro_bonus, ...} Intro = intro_bonus
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   435
  | locality_bonus {elim_bonus, ...} Elim = elim_bonus
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   436
  | locality_bonus {simp_bonus, ...} Simp = simp_bonus
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   437
  | locality_bonus {local_bonus, ...} Local = local_bonus
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   438
  | locality_bonus {assum_bonus, ...} Assum = assum_bonus
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   439
  | locality_bonus {chained_bonus, ...} Chained = chained_bonus
38751
01c4d14b2a61 add a bonus for chained facts, since they are likely to be relevant;
blanchet
parents: 38749
diff changeset
   440
40418
8b73059e97a1 better detection of completely irrelevant facts
blanchet
parents: 40408
diff changeset
   441
fun is_odd_const_name s =
8b73059e97a1 better detection of completely irrelevant facts
blanchet
parents: 40408
diff changeset
   442
  s = abs_name orelse String.isPrefix skolem_prefix s orelse
8b73059e97a1 better detection of completely irrelevant facts
blanchet
parents: 40408
diff changeset
   443
  String.isSuffix theory_const_suffix s
8b73059e97a1 better detection of completely irrelevant facts
blanchet
parents: 40408
diff changeset
   444
40204
da97d75e20e6 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents: 40191
diff changeset
   445
fun fact_weight fudge loc const_tab relevant_consts fact_consts =
da97d75e20e6 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents: 40191
diff changeset
   446
  case fact_consts |> List.partition (pconst_hyper_mem I relevant_consts)
da97d75e20e6 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents: 40191
diff changeset
   447
                   ||> filter_out (pconst_hyper_mem swap relevant_consts) of
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   448
    ([], _) => 0.0
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   449
  | (rel, irrel) =>
40418
8b73059e97a1 better detection of completely irrelevant facts
blanchet
parents: 40408
diff changeset
   450
    if forall (forall (is_odd_const_name o fst)) [rel, irrel] then
40371
8fe3c26c49af ignore facts with only theory constants in them
blanchet
parents: 40369
diff changeset
   451
      0.0
8fe3c26c49af ignore facts with only theory constants in them
blanchet
parents: 40369
diff changeset
   452
    else
8fe3c26c49af ignore facts with only theory constants in them
blanchet
parents: 40369
diff changeset
   453
      let
8fe3c26c49af ignore facts with only theory constants in them
blanchet
parents: 40369
diff changeset
   454
        val irrel = irrel |> filter_out (pconst_mem swap rel)
8fe3c26c49af ignore facts with only theory constants in them
blanchet
parents: 40369
diff changeset
   455
        val rel_weight =
8fe3c26c49af ignore facts with only theory constants in them
blanchet
parents: 40369
diff changeset
   456
          0.0 |> fold (curry (op +) o rel_pconst_weight fudge const_tab) rel
8fe3c26c49af ignore facts with only theory constants in them
blanchet
parents: 40369
diff changeset
   457
        val irrel_weight =
8fe3c26c49af ignore facts with only theory constants in them
blanchet
parents: 40369
diff changeset
   458
          ~ (locality_bonus fudge loc)
8fe3c26c49af ignore facts with only theory constants in them
blanchet
parents: 40369
diff changeset
   459
          |> fold (curry (op +) o irrel_pconst_weight fudge const_tab) irrel
8fe3c26c49af ignore facts with only theory constants in them
blanchet
parents: 40369
diff changeset
   460
        val res = rel_weight / (rel_weight + irrel_weight)
8fe3c26c49af ignore facts with only theory constants in them
blanchet
parents: 40369
diff changeset
   461
      in if Real.isFinite res then res else 0.0 end
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   462
40369
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40251
diff changeset
   463
fun pconsts_in_fact thy is_built_in_const t =
38825
4ec3cbd95f25 rename and simplify
blanchet
parents: 38824
diff changeset
   464
  Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
40369
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40251
diff changeset
   465
              (pconsts_in_terms thy is_built_in_const true (SOME true) [t]) []
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40251
diff changeset
   466
fun pair_consts_fact thy is_built_in_const fudge fact =
40204
da97d75e20e6 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents: 40191
diff changeset
   467
  case fact |> snd |> theory_const_prop_of fudge
40369
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40251
diff changeset
   468
            |> pconsts_in_fact thy is_built_in_const of
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   469
    [] => NONE
40204
da97d75e20e6 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents: 40191
diff changeset
   470
  | consts => SOME ((fact, consts), NONE)
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   471
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   472
type annotated_thm =
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   473
  (((unit -> string) * locality) * thm) * (string * ptype) list
37505
d9af5c01dc4a added code to optionally perform fact filtering on the original (non-CNF) formulas
blanchet
parents: 37504
diff changeset
   474
38904
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   475
fun take_most_relevant max_relevant remaining_max
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   476
        ({max_imperfect, max_imperfect_exp, ...} : relevance_fudge) 
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   477
        (candidates : (annotated_thm * real) list) =
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   478
  let
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   479
    val max_imperfect =
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   480
      Real.ceil (Math.pow (max_imperfect,
38904
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   481
                    Math.pow (Real.fromInt remaining_max
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   482
                              / Real.fromInt max_relevant, max_imperfect_exp)))
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   483
    val (perfect, imperfect) =
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   484
      candidates |> sort (Real.compare o swap o pairself snd)
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   485
                 |> take_prefix (fn (_, w) => w > 0.99999)
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   486
    val ((accepts, more_rejects), rejects) =
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   487
      chop max_imperfect imperfect |>> append perfect |>> chop remaining_max
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   488
  in
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   489
    trace_msg (fn () =>
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   490
        "Actually passed (" ^ Int.toString (length accepts) ^ " of " ^
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   491
        Int.toString (length candidates) ^ "): " ^
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   492
        (accepts |> map (fn ((((name, _), _), _), weight) =>
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   493
                            name () ^ " [" ^ Real.toString weight ^ "]")
38745
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   494
                 |> commas));
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   495
    (accepts, more_rejects @ rejects)
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   496
  end
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   497
40369
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40251
diff changeset
   498
fun if_empty_replace_with_locality thy is_built_in_const facts loc tab =
38819
71c9f61516cd if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents: 38818
diff changeset
   499
  if Symtab.is_empty tab then
40369
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40251
diff changeset
   500
    pconsts_in_terms thy is_built_in_const false (SOME false)
38819
71c9f61516cd if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents: 38818
diff changeset
   501
        (map_filter (fn ((_, loc'), th) =>
40204
da97d75e20e6 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents: 40191
diff changeset
   502
                        if loc' = loc then SOME (prop_of th) else NONE) facts)
38819
71c9f61516cd if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents: 38818
diff changeset
   503
  else
71c9f61516cd if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents: 38818
diff changeset
   504
    tab
71c9f61516cd if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents: 38818
diff changeset
   505
41158
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   506
fun add_arities is_built_in_const th =
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   507
  let
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   508
    fun aux _ _ NONE = NONE
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   509
      | aux t args (SOME tab) =
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   510
        case t of
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   511
          t1 $ t2 => SOME tab |> aux t1 (t2 :: args) |> aux t2 []
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   512
        | Const (x as (s, _)) =>
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   513
          (if is_built_in_const x args then
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   514
             SOME tab
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   515
           else case Symtab.lookup tab s of
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   516
             NONE => SOME (Symtab.update (s, length args) tab)
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   517
           | SOME n => if n = length args then SOME tab else NONE)
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   518
        | _ => SOME tab
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   519
  in aux (prop_of th) [] end
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   520
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   521
fun needs_ext is_built_in_const facts =
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   522
  fold (add_arities is_built_in_const o snd) facts (SOME Symtab.empty)
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   523
  |> is_none
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   524
40369
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40251
diff changeset
   525
fun relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   526
        (fudge as {threshold_divisor, ridiculous_threshold, ...})
40204
da97d75e20e6 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents: 40191
diff changeset
   527
        ({add, del, ...} : relevance_override) facts goal_ts =
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   528
  let
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   529
    val thy = ProofContext.theory_of ctxt
40204
da97d75e20e6 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents: 40191
diff changeset
   530
    val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty
38819
71c9f61516cd if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents: 38818
diff changeset
   531
    val goal_const_tab =
40369
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40251
diff changeset
   532
      pconsts_in_terms thy is_built_in_const false (SOME false) goal_ts
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40251
diff changeset
   533
      |> fold (if_empty_replace_with_locality thy is_built_in_const facts)
38993
504b9e1efd33 give priority to assumptions in structured proofs
blanchet
parents: 38992
diff changeset
   534
              [Chained, Assum, Local]
39012
96d97d1c676f cosmetics
blanchet
parents: 38997
diff changeset
   535
    val add_ths = Attrib.eval_thms ctxt add
96d97d1c676f cosmetics
blanchet
parents: 38997
diff changeset
   536
    val del_ths = Attrib.eval_thms ctxt del
40204
da97d75e20e6 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents: 40191
diff changeset
   537
    val facts = facts |> filter_out (member Thm.eq_thm del_ths o snd)
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   538
    fun iter j remaining_max threshold rel_const_tab hopeless hopeful =
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   539
      let
40191
257d2e06bfb8 put theorems added using "add:" at the beginning of the list returned by the relevance filter, so that they don't get truncated away
blanchet
parents: 40071
diff changeset
   540
        fun relevant [] _ [] =
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   541
            (* Nothing has been added this iteration. *)
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   542
            if j = 0 andalso threshold >= ridiculous_threshold then
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   543
              (* First iteration? Try again. *)
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   544
              iter 0 max_relevant (threshold / threshold_divisor) rel_const_tab
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   545
                   hopeless hopeful
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   546
            else
40191
257d2e06bfb8 put theorems added using "add:" at the beginning of the list returned by the relevance filter, so that they don't get truncated away
blanchet
parents: 40071
diff changeset
   547
              []
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   548
          | relevant candidates rejects [] =
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   549
            let
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   550
              val (accepts, more_rejects) =
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   551
                take_most_relevant max_relevant remaining_max fudge candidates
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   552
              val rel_const_tab' =
38745
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   553
                rel_const_tab
41066
3890ef4e02f9 pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
blanchet
parents: 40418
diff changeset
   554
                |> fold (add_pconst_to_table false) (maps (snd o fst) accepts)
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   555
              fun is_dirty (c, _) =
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   556
                Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c
38745
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   557
              val (hopeful_rejects, hopeless_rejects) =
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   558
                 (rejects @ hopeless, ([], []))
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   559
                 |-> fold (fn (ax as (_, consts), old_weight) =>
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   560
                              if exists is_dirty consts then
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   561
                                apfst (cons (ax, NONE))
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   562
                              else
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   563
                                apsnd (cons (ax, old_weight)))
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   564
                 |>> append (more_rejects
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   565
                             |> map (fn (ax as (_, consts), old_weight) =>
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   566
                                        (ax, if exists is_dirty consts then NONE
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   567
                                             else SOME old_weight)))
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   568
              val threshold =
38822
aa0101e618e2 fix threshold computation + remove "op =" from relevant constants
blanchet
parents: 38821
diff changeset
   569
                1.0 - (1.0 - threshold)
aa0101e618e2 fix threshold computation + remove "op =" from relevant constants
blanchet
parents: 38821
diff changeset
   570
                      * Math.pow (decay, Real.fromInt (length accepts))
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   571
              val remaining_max = remaining_max - length accepts
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   572
            in
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   573
              trace_msg (fn () => "New or updated constants: " ^
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   574
                  commas (rel_const_tab' |> Symtab.dest
38822
aa0101e618e2 fix threshold computation + remove "op =" from relevant constants
blanchet
parents: 38821
diff changeset
   575
                          |> subtract (op =) (rel_const_tab |> Symtab.dest)
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   576
                          |> map string_for_hyper_pconst));
38745
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   577
              map (fst o fst) accepts @
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   578
              (if remaining_max = 0 then
40191
257d2e06bfb8 put theorems added using "add:" at the beginning of the list returned by the relevance filter, so that they don't get truncated away
blanchet
parents: 40071
diff changeset
   579
                 []
38745
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   580
               else
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   581
                 iter (j + 1) remaining_max threshold rel_const_tab'
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   582
                      hopeless_rejects hopeful_rejects)
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   583
            end
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   584
          | relevant candidates rejects
40204
da97d75e20e6 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents: 40191
diff changeset
   585
                     (((ax as (((_, loc), _), fact_consts)), cached_weight)
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   586
                      :: hopeful) =
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   587
            let
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   588
              val weight =
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   589
                case cached_weight of
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   590
                  SOME w => w
40204
da97d75e20e6 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents: 40191
diff changeset
   591
                | NONE => fact_weight fudge loc const_tab rel_const_tab
da97d75e20e6 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents: 40191
diff changeset
   592
                                      fact_consts
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   593
            in
38741
7635bf8918a1 get rid of "defs_relevant" feature;
blanchet
parents: 38739
diff changeset
   594
              if weight >= threshold then
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   595
                relevant ((ax, weight) :: candidates) rejects hopeful
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   596
              else
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   597
                relevant candidates ((ax, weight) :: rejects) hopeful
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   598
            end
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   599
        in
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   600
          trace_msg (fn () =>
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   601
              "ITERATION " ^ string_of_int j ^ ": current threshold: " ^
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   602
              Real.toString threshold ^ ", constants: " ^
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   603
              commas (rel_const_tab |> Symtab.dest
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   604
                      |> filter (curry (op <>) [] o snd)
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   605
                      |> map string_for_hyper_pconst));
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   606
          relevant [] [] hopeful
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   607
        end
41158
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   608
    fun add_facts ths accepts =
41167
b05014180288 move facts supplied with "add:" to the front, so that they get a better weight (SMT)
blanchet
parents: 41159
diff changeset
   609
      (facts |> filter (member Thm.eq_thm ths o snd)) @
b05014180288 move facts supplied with "add:" to the front, so that they get a better weight (SMT)
blanchet
parents: 41159
diff changeset
   610
      (accepts |> filter_out (member Thm.eq_thm ths o snd))
40408
0d0acdf068b8 always honor the max relevant constraint
blanchet
parents: 40375
diff changeset
   611
      |> take max_relevant
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   612
  in
40369
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40251
diff changeset
   613
    facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)
40204
da97d75e20e6 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents: 40191
diff changeset
   614
          |> iter 0 max_relevant threshold0 goal_const_tab []
41158
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   615
          |> not (null add_ths) ? add_facts add_ths
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   616
          |> (fn accepts =>
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   617
                 accepts |> needs_ext is_built_in_const accepts
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   618
                            ? add_facts @{thms ext})
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   619
          |> tap (fn accepts => trace_msg (fn () =>
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   620
                      "Total relevant: " ^ Int.toString (length accepts)))
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   621
  end
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   622
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   623
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   624
(***************************************************************)
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   625
(* Retrieving and filtering lemmas                             *)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   626
(***************************************************************)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   627
33022
c95102496490 Removal of the unused atpset concept, the atp attribute and some related code.
paulson
parents: 32994
diff changeset
   628
(*** retrieve lemmas and filter them ***)
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   629
20757
fe84fe0dfd30 Definitions produced by packages are now blacklisted.
paulson
parents: 20661
diff changeset
   630
(*Reject theorems with names like "List.filter.filter_list_def" or
21690
552d20ff9a95 Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents: 21588
diff changeset
   631
  "Accessible_Part.acc.defs", as these are definitions arising from packages.*)
20757
fe84fe0dfd30 Definitions produced by packages are now blacklisted.
paulson
parents: 20661
diff changeset
   632
fun is_package_def a =
40205
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   633
  let val names = Long_Name.explode a in
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   634
    (length names > 2 andalso not (hd names = "local") andalso
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   635
     String.isSuffix "_def" a) orelse String.isSuffix "_defs" a
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   636
  end
20757
fe84fe0dfd30 Definitions produced by packages are now blacklisted.
paulson
parents: 20661
diff changeset
   637
38937
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   638
fun mk_fact_table f xs =
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   639
  fold (Termtab.update o `(prop_of o f)) xs Termtab.empty
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   640
fun uniquify xs = Termtab.fold (cons o snd) (mk_fact_table snd xs) []
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   641
37626
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   642
(* FIXME: put other record thms here, or declare as "no_atp" *)
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   643
val multi_base_blacklist =
41199
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   644
  ["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   645
   "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   646
   "weak_case_cong"]
38682
3a203da3f89b weed out junk in relevance filter
blanchet
parents: 38681
diff changeset
   647
  |> map (prefix ".")
37626
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   648
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   649
val max_lambda_nesting = 3
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   650
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   651
fun term_has_too_many_lambdas max (t1 $ t2) =
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   652
    exists (term_has_too_many_lambdas max) [t1, t2]
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   653
  | term_has_too_many_lambdas max (Abs (_, _, t)) =
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   654
    max = 0 orelse term_has_too_many_lambdas (max - 1) t
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   655
  | term_has_too_many_lambdas _ _ = false
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   656
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   657
(* Don't count nested lambdas at the level of formulas, since they are
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   658
   quantifiers. *)
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   659
fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   660
    formula_has_too_many_lambdas (T :: Ts) t
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   661
  | formula_has_too_many_lambdas Ts t =
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   662
    if is_formula_type (fastype_of1 (Ts, t)) then
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   663
      exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   664
    else
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   665
      term_has_too_many_lambdas max_lambda_nesting t
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   666
38692
89d3550d8e16 cosmetics
blanchet
parents: 38689
diff changeset
   667
(* The max apply depth of any "metis" call in "Metis_Examples" (on 2007-10-31)
37626
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   668
   was 11. *)
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   669
val max_apply_depth = 15
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   670
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   671
fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   672
  | apply_depth (Abs (_, _, t)) = apply_depth t
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   673
  | apply_depth _ = 0
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   674
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   675
fun is_formula_too_complex t =
38085
cc44e887246c avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents: 38027
diff changeset
   676
  apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas [] t
37626
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   677
39946
78faa9b31202 move Metis into Plain
blanchet
parents: 39896
diff changeset
   678
(* FIXME: Extend to "Meson" and "Metis" *)
37543
2e733b0a963c a76ace919f1c wasn't quite right; second try
blanchet
parents: 37538
diff changeset
   679
val exists_sledgehammer_const =
37626
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   680
  exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   681
38904
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   682
(* FIXME: make more reliable *)
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   683
val exists_low_level_class_const =
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   684
  exists_Const (fn (s, _) =>
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   685
     String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s)
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   686
38821
d0275b6c4e9d avoid needless "that" fact
blanchet
parents: 38820
diff changeset
   687
fun is_metastrange_theorem th =
37626
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   688
  case head_of (concl_of th) of
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   689
      Const (a, _) => (a <> @{const_name Trueprop} andalso
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   690
                       a <> @{const_name "=="})
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   691
    | _ => false
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   692
38821
d0275b6c4e9d avoid needless "that" fact
blanchet
parents: 38820
diff changeset
   693
fun is_that_fact th =
d0275b6c4e9d avoid needless "that" fact
blanchet
parents: 38820
diff changeset
   694
  String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th)
d0275b6c4e9d avoid needless "that" fact
blanchet
parents: 38820
diff changeset
   695
  andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
d0275b6c4e9d avoid needless "that" fact
blanchet
parents: 38820
diff changeset
   696
                           | _ => false) (prop_of th)
d0275b6c4e9d avoid needless "that" fact
blanchet
parents: 38820
diff changeset
   697
37626
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   698
val type_has_top_sort =
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   699
  exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   700
38085
cc44e887246c avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents: 38027
diff changeset
   701
(**** Predicates to detect unwanted facts (prolific or likely to cause
37347
635425a442e8 show more respect for user-specified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents: 37345
diff changeset
   702
      unsoundness) ****)
21470
7c1b59ddcd56 Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents: 21431
diff changeset
   703
38289
74dd8dd33512 adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents: 38279
diff changeset
   704
(* Too general means, positive equality literal with a variable X as one
74dd8dd33512 adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents: 38279
diff changeset
   705
   operand, when X does not occur properly in the other operand. This rules out
74dd8dd33512 adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents: 38279
diff changeset
   706
   clearly inconsistent facts such as X = a | X = b, though it by no means
74dd8dd33512 adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents: 38279
diff changeset
   707
   guarantees soundness. *)
21470
7c1b59ddcd56 Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents: 21431
diff changeset
   708
38289
74dd8dd33512 adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents: 38279
diff changeset
   709
(* Unwanted equalities are those between a (bound or schematic) variable that
74dd8dd33512 adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents: 38279
diff changeset
   710
   does not properly occur in the second operand. *)
38607
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   711
val is_exhaustive_finite =
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   712
  let
38629
3387432c18af more work on finite axiom detection
blanchet
parents: 38627
diff changeset
   713
    fun is_bad_equal (Var z) t =
3387432c18af more work on finite axiom detection
blanchet
parents: 38627
diff changeset
   714
        not (exists_subterm (fn Var z' => z = z' | _ => false) t)
3387432c18af more work on finite axiom detection
blanchet
parents: 38627
diff changeset
   715
      | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j))
3387432c18af more work on finite axiom detection
blanchet
parents: 38627
diff changeset
   716
      | is_bad_equal _ _ = false
3387432c18af more work on finite axiom detection
blanchet
parents: 38627
diff changeset
   717
    fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1
38607
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   718
    fun do_formula pos t =
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   719
      case (pos, t) of
38615
4e1d828ee514 improve "x = A | x = B | x = C"-style axiom detection
blanchet
parents: 38611
diff changeset
   720
        (_, @{const Trueprop} $ t1) => do_formula pos t1
38607
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   721
      | (true, Const (@{const_name all}, _) $ Abs (_, _, t')) =>
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   722
        do_formula pos t'
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   723
      | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) =>
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   724
        do_formula pos t'
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   725
      | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) =>
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   726
        do_formula pos t'
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   727
      | (_, @{const "==>"} $ t1 $ t2) =>
38629
3387432c18af more work on finite axiom detection
blanchet
parents: 38627
diff changeset
   728
        do_formula (not pos) t1 andalso
3387432c18af more work on finite axiom detection
blanchet
parents: 38627
diff changeset
   729
        (t2 = @{prop False} orelse do_formula pos t2)
38786
e46e7a9cb622 formerly unnamed infix impliciation now named HOL.implies
haftmann
parents: 38752
diff changeset
   730
      | (_, @{const HOL.implies} $ t1 $ t2) =>
38629
3387432c18af more work on finite axiom detection
blanchet
parents: 38627
diff changeset
   731
        do_formula (not pos) t1 andalso
3387432c18af more work on finite axiom detection
blanchet
parents: 38627
diff changeset
   732
        (t2 = @{const False} orelse do_formula pos t2)
38607
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   733
      | (_, @{const Not} $ t1) => do_formula (not pos) t1
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   734
      | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   735
      | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38829
diff changeset
   736
      | (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2
38607
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   737
      | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   738
      | _ => false
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   739
  in do_formula true end
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   740
38592
ae6bb801e583 bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq")
blanchet
parents: 38587
diff changeset
   741
fun has_bound_or_var_of_type tycons =
ae6bb801e583 bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq")
blanchet
parents: 38587
diff changeset
   742
  exists_subterm (fn Var (_, Type (s, _)) => member (op =) tycons s
ae6bb801e583 bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq")
blanchet
parents: 38587
diff changeset
   743
                   | Abs (_, Type (s, _), _) => member (op =) tycons s
ae6bb801e583 bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq")
blanchet
parents: 38587
diff changeset
   744
                   | _ => false)
21431
ef9080e7dbbc Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents: 21397
diff changeset
   745
38085
cc44e887246c avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents: 38027
diff changeset
   746
(* Facts are forbidden to contain variables of these types. The typical reason
37347
635425a442e8 show more respect for user-specified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents: 37345
diff changeset
   747
   is that they lead to unsoundness. Note that "unit" satisfies numerous
38085
cc44e887246c avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents: 38027
diff changeset
   748
   equations like "?x = ()". The resulting clauses will have no type constraint,
37347
635425a442e8 show more respect for user-specified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents: 37345
diff changeset
   749
   yielding false proofs. Even "bool" leads to many unsound proofs, though only
635425a442e8 show more respect for user-specified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents: 37345
diff changeset
   750
   for higher-order problems. *)
38592
ae6bb801e583 bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq")
blanchet
parents: 38587
diff changeset
   751
val dangerous_types = [@{type_name unit}, @{type_name bool}, @{type_name prop}];
22217
a5d983f7113f Tidying; more debugging information. New reference unwanted_types.
paulson
parents: 22193
diff changeset
   752
38085
cc44e887246c avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents: 38027
diff changeset
   753
(* Facts containing variables of type "unit" or "bool" or of the form
38290
581a402a80f0 prevent ATP thread for staying around for 1 minute if an exception occurred earlier;
blanchet
parents: 38289
diff changeset
   754
   "ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types
581a402a80f0 prevent ATP thread for staying around for 1 minute if an exception occurred earlier;
blanchet
parents: 38289
diff changeset
   755
   are omitted. *)
41138
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41066
diff changeset
   756
fun is_dangerous_term no_dangerous_types t =
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41066
diff changeset
   757
  not no_dangerous_types andalso
38679
2cfd0777580f destroy elim rules before checking for finite exhaustive facts
blanchet
parents: 38652
diff changeset
   758
  let val t = transform_elim_term t in
2cfd0777580f destroy elim rules before checking for finite exhaustive facts
blanchet
parents: 38652
diff changeset
   759
    has_bound_or_var_of_type dangerous_types t orelse
2cfd0777580f destroy elim rules before checking for finite exhaustive facts
blanchet
parents: 38652
diff changeset
   760
    is_exhaustive_finite t
2cfd0777580f destroy elim rules before checking for finite exhaustive facts
blanchet
parents: 38652
diff changeset
   761
  end
21470
7c1b59ddcd56 Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents: 21431
diff changeset
   762
41138
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41066
diff changeset
   763
fun is_theorem_bad_for_atps no_dangerous_types thm =
38627
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   764
  let val t = prop_of thm in
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   765
    is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
41138
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41066
diff changeset
   766
    is_dangerous_term no_dangerous_types t orelse
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41066
diff changeset
   767
    exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41066
diff changeset
   768
    is_metastrange_theorem thm orelse is_that_fact thm
38627
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   769
  end
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   770
38937
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   771
fun clasimpset_rules_of ctxt =
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   772
  let
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   773
    val {safeIs, safeEs, hazIs, hazEs, ...} = ctxt |> claset_of |> rep_cs
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   774
    val intros = safeIs @ hazIs
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   775
    val elims = map Classical.classical_rule (safeEs @ hazEs)
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   776
    val simps = ctxt |> simpset_of |> dest_ss |> #simps |> map snd
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   777
  in (mk_fact_table I intros, mk_fact_table I elims, mk_fact_table I simps) end
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   778
41138
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41066
diff changeset
   779
fun all_facts ctxt reserved no_dangerous_types
40205
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   780
              ({intro_bonus, elim_bonus, simp_bonus, ...} : relevance_fudge)
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   781
              add_ths chained_ths =
38627
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   782
  let
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   783
    val thy = ProofContext.theory_of ctxt
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39367
diff changeset
   784
    val global_facts = Global_Theory.facts_of thy
38644
25bbbaf7ce65 don't penalize abstractions in relevance filter + support nameless `foo`-style facts
blanchet
parents: 38629
diff changeset
   785
    val local_facts = ProofContext.facts_of ctxt
25bbbaf7ce65 don't penalize abstractions in relevance filter + support nameless `foo`-style facts
blanchet
parents: 38629
diff changeset
   786
    val named_locals = local_facts |> Facts.dest_static []
38993
504b9e1efd33 give priority to assumptions in structured proofs
blanchet
parents: 38992
diff changeset
   787
    val assms = Assumption.all_assms_of ctxt
504b9e1efd33 give priority to assumptions in structured proofs
blanchet
parents: 38992
diff changeset
   788
    fun is_assum th = exists (fn ct => prop_of th aconv term_of ct) assms
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   789
    val is_chained = member Thm.eq_thm chained_ths
38937
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   790
    val (intros, elims, simps) =
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   791
      if exists (curry (op <) 0.0) [intro_bonus, elim_bonus, simp_bonus] then
38937
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   792
        clasimpset_rules_of ctxt
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   793
      else
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   794
        (Termtab.empty, Termtab.empty, Termtab.empty)
38738
0ce517c1970f make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts
blanchet
parents: 38699
diff changeset
   795
    fun is_good_unnamed_local th =
38820
d0f98bd81a85 add nameless chained facts to the pool of things known to Sledgehammer
blanchet
parents: 38819
diff changeset
   796
      not (Thm.has_name_hint th) andalso
38738
0ce517c1970f make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts
blanchet
parents: 38699
diff changeset
   797
      forall (fn (_, ths) => not (member Thm.eq_thm ths th)) named_locals
38644
25bbbaf7ce65 don't penalize abstractions in relevance filter + support nameless `foo`-style facts
blanchet
parents: 38629
diff changeset
   798
    val unnamed_locals =
38820
d0f98bd81a85 add nameless chained facts to the pool of things known to Sledgehammer
blanchet
parents: 38819
diff changeset
   799
      union Thm.eq_thm (Facts.props local_facts) chained_ths
d0f98bd81a85 add nameless chained facts to the pool of things known to Sledgehammer
blanchet
parents: 38819
diff changeset
   800
      |> filter is_good_unnamed_local |> map (pair "" o single)
38627
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   801
    val full_space =
38738
0ce517c1970f make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts
blanchet
parents: 38699
diff changeset
   802
      Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   803
    fun add_facts global foldx facts =
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   804
      foldx (fn (name0, ths) =>
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   805
        if name0 <> "" andalso
39012
96d97d1c676f cosmetics
blanchet
parents: 38997
diff changeset
   806
           forall (not o member Thm.eq_thm add_ths) ths andalso
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   807
           (Facts.is_concealed facts name0 orelse
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   808
            (respect_no_atp andalso is_package_def name0) orelse
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   809
            exists (fn s => String.isSuffix s name0) multi_base_blacklist orelse
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   810
            String.isSuffix "_def_raw" (* FIXME: crude hack *) name0) then
38627
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   811
          I
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   812
        else
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   813
          let
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   814
            val multi = length ths > 1
41199
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   815
            val backquotify =
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   816
              enclose "`" "`" o string_for_term ctxt o close_form o prop_of
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   817
            fun check_thms a =
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   818
              case try (ProofContext.get_thms ctxt) a of
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   819
                NONE => false
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   820
              | SOME ths' => Thm.eq_thms (ths, ths')
38627
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   821
          in
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   822
            pair 1
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   823
            #> fold (fn th => fn (j, rest) =>
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   824
                 (j + 1,
41138
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41066
diff changeset
   825
                  if is_theorem_bad_for_atps no_dangerous_types th andalso
39012
96d97d1c676f cosmetics
blanchet
parents: 38997
diff changeset
   826
                     not (member Thm.eq_thm add_ths th) then
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   827
                    rest
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   828
                  else
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   829
                    (((fn () =>
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   830
                          if name0 = "" then
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   831
                            th |> backquotify
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   832
                          else
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   833
                            let
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   834
                              val name1 = Facts.extern facts name0
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   835
                              val name2 = Name_Space.extern full_space name0
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   836
                            in
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   837
                              case find_first check_thms [name1, name2, name0] of
40375
db690d38e4b9 fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents: 40373
diff changeset
   838
                                SOME name => make_name reserved multi j name
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   839
                              | NONE => ""
38937
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   840
                            end),
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   841
                      let val t = prop_of th in
40071
658a37c80b53 generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents: 40070
diff changeset
   842
                        if is_chained th then
658a37c80b53 generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents: 40070
diff changeset
   843
                          Chained
38993
504b9e1efd33 give priority to assumptions in structured proofs
blanchet
parents: 38992
diff changeset
   844
                        else if global then
504b9e1efd33 give priority to assumptions in structured proofs
blanchet
parents: 38992
diff changeset
   845
                          if Termtab.defined intros t then Intro
504b9e1efd33 give priority to assumptions in structured proofs
blanchet
parents: 38992
diff changeset
   846
                          else if Termtab.defined elims t then Elim
504b9e1efd33 give priority to assumptions in structured proofs
blanchet
parents: 38992
diff changeset
   847
                          else if Termtab.defined simps t then Simp
504b9e1efd33 give priority to assumptions in structured proofs
blanchet
parents: 38992
diff changeset
   848
                          else General
504b9e1efd33 give priority to assumptions in structured proofs
blanchet
parents: 38992
diff changeset
   849
                        else
504b9e1efd33 give priority to assumptions in structured proofs
blanchet
parents: 38992
diff changeset
   850
                          if is_assum th then Assum else Local
38937
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   851
                      end),
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   852
                      (multi, th)) :: rest)) ths
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   853
            #> snd
38627
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   854
          end)
38644
25bbbaf7ce65 don't penalize abstractions in relevance filter + support nameless `foo`-style facts
blanchet
parents: 38629
diff changeset
   855
  in
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   856
    [] |> add_facts false fold local_facts (unnamed_locals @ named_locals)
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   857
       |> add_facts true Facts.fold_static global_facts global_facts
38644
25bbbaf7ce65 don't penalize abstractions in relevance filter + support nameless `foo`-style facts
blanchet
parents: 38629
diff changeset
   858
  end
38627
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   859
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   860
(* The single-name theorems go after the multiple-name ones, so that single
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   861
   names are preferred when both are available. *)
40205
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   862
fun rearrange_facts ctxt respect_no_atp =
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   863
  List.partition (fst o snd) #> op @ #> map (apsnd snd)
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   864
  #> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd)
38627
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   865
41199
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   866
fun external_frees t =
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   867
  [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   868
41138
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41066
diff changeset
   869
fun relevant_facts ctxt no_dangerous_types (threshold0, threshold1)
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41066
diff changeset
   870
                   max_relevant is_built_in_const fudge
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41066
diff changeset
   871
                   (override as {add, only, ...}) chained_ths hyp_ts concl_t =
37538
97ab019d5ac8 make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents: 37537
diff changeset
   872
  let
41200
6cc9b6fd7f6f add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents: 41199
diff changeset
   873
    val thy = ProofContext.theory_of ctxt
38822
aa0101e618e2 fix threshold computation + remove "op =" from relevant constants
blanchet
parents: 38821
diff changeset
   874
    val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
aa0101e618e2 fix threshold computation + remove "op =" from relevant constants
blanchet
parents: 38821
diff changeset
   875
                          1.0 / Real.fromInt (max_relevant + 1))
39012
96d97d1c676f cosmetics
blanchet
parents: 38997
diff changeset
   876
    val add_ths = Attrib.eval_thms ctxt add
38696
4c6b65d6a135 quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents: 38692
diff changeset
   877
    val reserved = reserved_isar_keyword_table ()
41199
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   878
    val ind_stmt =
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   879
      Logic.list_implies (hyp_ts |> filter_out (null o external_frees), concl_t)
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   880
      |> atomize_term
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   881
    val ind_stmt_xs = external_frees ind_stmt
40204
da97d75e20e6 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents: 40191
diff changeset
   882
    val facts =
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   883
      (if only then
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   884
         maps (map (fn ((name, loc), th) => ((K name, loc), (true, th)))
40205
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   885
               o fact_from_ref ctxt reserved chained_ths) add
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   886
       else
41138
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41066
diff changeset
   887
         all_facts ctxt reserved no_dangerous_types fudge add_ths chained_ths)
41199
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   888
      |> maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
40205
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   889
      |> rearrange_facts ctxt (respect_no_atp andalso not only)
38937
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   890
      |> uniquify
37538
97ab019d5ac8 make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents: 37537
diff changeset
   891
  in
40204
da97d75e20e6 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents: 40191
diff changeset
   892
    trace_msg (fn () => "Considering " ^ Int.toString (length facts) ^
da97d75e20e6 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents: 40191
diff changeset
   893
                        " facts");
39366
f58fbb959826 handle relevance filter corner cases more gracefully;
blanchet
parents: 39265
diff changeset
   894
    (if only orelse threshold1 < 0.0 then
40204
da97d75e20e6 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents: 40191
diff changeset
   895
       facts
39366
f58fbb959826 handle relevance filter corner cases more gracefully;
blanchet
parents: 39265
diff changeset
   896
     else if threshold0 > 1.0 orelse threshold0 > threshold1 orelse
f58fbb959826 handle relevance filter corner cases more gracefully;
blanchet
parents: 39265
diff changeset
   897
             max_relevant = 0 then
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   898
       []
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   899
     else
41200
6cc9b6fd7f6f add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents: 41199
diff changeset
   900
       ((concl_t |> theory_constify fudge (Context.theory_name thy)) :: hyp_ts)
6cc9b6fd7f6f add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents: 41199
diff changeset
   901
       |> relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
6cc9b6fd7f6f add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents: 41199
diff changeset
   902
                           fudge override facts)
38822
aa0101e618e2 fix threshold computation + remove "op =" from relevant constants
blanchet
parents: 38821
diff changeset
   903
    |> map (apfst (apfst (fn f => f ())))
37538
97ab019d5ac8 make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents: 37537
diff changeset
   904
  end
30536
07b4f050e4df split relevance-filter and writing of problem-files;
immler@in.tum.de
parents: 30364
diff changeset
   905
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
   906
end;