src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
author blanchet
Wed, 31 Aug 2011 11:52:03 +0200
changeset 44625 4a1132815a70
parent 44586 eeba1eedf32d
child 44783 3634c6dba23f
permissions -rw-r--r--
more 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
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43066
diff changeset
    10
  type locality = ATP_Translate.locality
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 =
42738
2a9dcff63b80 remove unused parameter
blanchet
parents: 42735
diff changeset
    13
    {local_const_multiplier : real,
41159
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,
42735
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
    21
     chained_const_irrel_weight : real,
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    22
     intro_bonus : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    23
     elim_bonus : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    24
     simp_bonus : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    25
     local_bonus : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    26
     assum_bonus : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    27
     chained_bonus : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    28
     max_imperfect : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    29
     max_imperfect_exp : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    30
     threshold_divisor : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    31
     ridiculous_threshold : real}
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    32
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35963
diff changeset
    33
  type relevance_override =
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    34
    {add : (Facts.ref * Attrib.src list) list,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    35
     del : (Facts.ref * Attrib.src list) list,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    36
     only : bool}
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35963
diff changeset
    37
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42641
diff changeset
    38
  val trace : bool Config.T
42728
44cd74a419ce added configuration options for experimental features
blanchet
parents: 42702
diff changeset
    39
  val ignore_no_atp : bool Config.T
44cd74a419ce added configuration options for experimental features
blanchet
parents: 42702
diff changeset
    40
  val instantiate_inducts : bool Config.T
44462
d9a657c44380 more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents: 44400
diff changeset
    41
  val no_relevance_override : relevance_override
43351
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43324
diff changeset
    42
  val const_names_in_fact :
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43324
diff changeset
    43
    theory -> (string * typ -> term list -> bool * term list) -> term
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43324
diff changeset
    44
    -> string list
40205
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
    45
  val fact_from_ref :
38996
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
    46
    Proof.context -> unit Symtab.table -> thm list
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
    47
    -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
41767
44b2a0385001 export useful function (needed in a Sledgehammer-related experiment)
blanchet
parents: 41491
diff changeset
    48
  val all_facts :
44585
cfe7f4a68e51 added generation of induction rules
nik
parents: 44462
diff changeset
    49
    Proof.context -> bool -> 'a Symtab.table -> bool -> thm list -> thm list
43351
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43324
diff changeset
    50
    -> (((unit -> string) * locality) * thm) list
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43324
diff changeset
    51
  val nearly_all_facts :
44585
cfe7f4a68e51 added generation of induction rules
nik
parents: 44462
diff changeset
    52
    Proof.context -> bool -> relevance_override -> thm list -> term list -> term
43351
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43324
diff changeset
    53
    -> (((unit -> 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
    54
  val relevant_facts :
44625
4a1132815a70 more tuning
blanchet
parents: 44586
diff changeset
    55
    Proof.context -> real * real -> int
41336
0ea5b9c7d233 proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents: 41279
diff changeset
    56
    -> (string * typ -> term list -> bool * term list) -> relevance_fudge
41066
3890ef4e02f9 pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
blanchet
parents: 40418
diff changeset
    57
    -> relevance_override -> thm list -> term list -> term
43351
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43324
diff changeset
    58
    -> (((unit -> string) * locality) * thm) list
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    59
    -> ((string * locality) * thm) list
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    60
end;
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    61
38988
483879af0643 finished renaming
blanchet
parents: 38986
diff changeset
    62
structure Sledgehammer_Filter : SLEDGEHAMMER_FILTER =
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    63
struct
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    64
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43066
diff changeset
    65
open ATP_Translate
38652
e063be321438 perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents: 38644
diff changeset
    66
open Sledgehammer_Util
e063be321438 perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents: 38644
diff changeset
    67
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42641
diff changeset
    68
val trace =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42641
diff changeset
    69
  Attrib.setup_config_bool @{binding sledgehammer_filter_trace} (K false)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42641
diff changeset
    70
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
35826
1590abc3d42a renamed Sledgehammer structures
blanchet
parents: 35825
diff changeset
    71
41273
35ce17cd7967 made the relevance filter treat unatomizable facts like "atomize_all" properly (these result in problems that get E spinning seemingly forever);
blanchet
parents: 41211
diff changeset
    72
(* experimental features *)
42728
44cd74a419ce added configuration options for experimental features
blanchet
parents: 42702
diff changeset
    73
val ignore_no_atp =
44cd74a419ce added configuration options for experimental features
blanchet
parents: 42702
diff changeset
    74
  Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false)
44cd74a419ce added configuration options for experimental features
blanchet
parents: 42702
diff changeset
    75
val instantiate_inducts =
44cd74a419ce added configuration options for experimental features
blanchet
parents: 42702
diff changeset
    76
  Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false)
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
    77
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    78
type relevance_fudge =
42738
2a9dcff63b80 remove unused parameter
blanchet
parents: 42735
diff changeset
    79
  {local_const_multiplier : real,
41159
1e12d6495423 honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents: 41158
diff changeset
    80
   worse_irrel_freq : real,
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    81
   higher_order_irrel_weight : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    82
   abs_rel_weight : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    83
   abs_irrel_weight : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    84
   skolem_irrel_weight : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    85
   theory_const_rel_weight : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    86
   theory_const_irrel_weight : real,
42735
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
    87
   chained_const_irrel_weight : real,
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    88
   intro_bonus : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    89
   elim_bonus : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    90
   simp_bonus : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    91
   local_bonus : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    92
   assum_bonus : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    93
   chained_bonus : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    94
   max_imperfect : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    95
   max_imperfect_exp : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    96
   threshold_divisor : real,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    97
   ridiculous_threshold : real}
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
    98
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35963
diff changeset
    99
type relevance_override =
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   100
  {add : (Facts.ref * Attrib.src list) list,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   101
   del : (Facts.ref * Attrib.src list) list,
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   102
   only : bool}
21070
0a898140fea2 Added more debugging info
paulson
parents: 20995
diff changeset
   103
44462
d9a657c44380 more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents: 44400
diff changeset
   104
val no_relevance_override = {add = [], del = [], only = false}
d9a657c44380 more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents: 44400
diff changeset
   105
37616
c8d2d84d6011 always perform relevance filtering on original formulas
blanchet
parents: 37580
diff changeset
   106
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
   107
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
   108
val skolem_prefix = sledgehammer_prefix ^ "sko"
38992
542474156c66 introduce fudge factors to deal with "theory const"
blanchet
parents: 38988
diff changeset
   109
val theory_const_suffix = Long_Name.separator ^ " 1"
37616
c8d2d84d6011 always perform relevance filtering on original formulas
blanchet
parents: 37580
diff changeset
   110
40227
e31e3f0071d4 support non-identifier-like fact names in Sledgehammer (e.g., "my lemma") by quoting them
blanchet
parents: 40205
diff changeset
   111
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
   112
  Symtab.defined reserved s orelse
42290
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 41999
diff changeset
   113
  exists (not o Lexicon.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
   114
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
   115
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
   116
  (name |> needs_quoting reserved name ? quote) ^
41491
a2ad5b824051 eliminated Int.toString;
wenzelm
parents: 41336
diff changeset
   117
  (if multi then "(" ^ string_of_int j ^ ")" else "")
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   118
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
   119
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
   120
  | 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
   121
  | 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
   122
41279
e0400b05a62c escape backticks in altstrings
blanchet
parents: 41273
diff changeset
   123
val backquote =
e0400b05a62c escape backticks in altstrings
blanchet
parents: 41273
diff changeset
   124
  raw_explode #> map (fn "`" => "\\`" | s => s) #> implode #> enclose "`" "`"
40205
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   125
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
   126
  let
38996
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
   127
    val ths = Attrib.eval_thms ctxt [xthm]
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
   128
    val bracket =
41999
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41989
diff changeset
   129
      map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41989
diff changeset
   130
      |> implode
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
   131
    fun nth_name j =
38996
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
   132
      case xref of
41279
e0400b05a62c escape backticks in altstrings
blanchet
parents: 41273
diff changeset
   133
        Facts.Fact s => backquote s ^ bracket
38996
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
   134
      | 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
   135
      | 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
   136
        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
   137
      | 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
   138
        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
   139
                 (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
   140
        bracket
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   141
  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
   142
    (ths, (0, []))
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   143
    |-> fold (fn th => fn (j, rest) =>
43421
926bfe067a32 fixed soundness bug related to extensionality
blanchet
parents: 43351
diff changeset
   144
                 (j + 1,
926bfe067a32 fixed soundness bug related to extensionality
blanchet
parents: 43351
diff changeset
   145
                  ((nth_name j,
926bfe067a32 fixed soundness bug related to extensionality
blanchet
parents: 43351
diff changeset
   146
                    if member Thm.eq_thm_prop chained_ths th then Chained
926bfe067a32 fixed soundness bug related to extensionality
blanchet
parents: 43351
diff changeset
   147
                    else if Thm.eq_thm_prop (th, @{thm ext}) then Extensionality
926bfe067a32 fixed soundness bug related to extensionality
blanchet
parents: 43351
diff changeset
   148
                    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
   149
    |> snd
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   150
  end
37616
c8d2d84d6011 always perform relevance filtering on original formulas
blanchet
parents: 37580
diff changeset
   151
41199
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   152
(* This is a terrible hack. Free variables are sometimes code as "M__" when they
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   153
   are displayed as "M" and we want to avoid clashes with these. But sometimes
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   154
   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
   155
   free variables. In the worse case scenario, where the fact won't be resolved
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   156
   correctly, the user can fix it manually, e.g., by naming the fact in
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   157
   question. Ideally we would need nothing of it, but backticks just don't work
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   158
   with schematic variables. *)
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   159
fun all_prefixes_of s =
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   160
  map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   161
fun close_form t =
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   162
  (t, [] |> Term.add_free_names t |> maps all_prefixes_of)
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   163
  |> fold (fn ((s, i), T) => fn (t', taken) =>
43324
2b47822868e4 discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents: 43245
diff changeset
   164
              let val s' = singleton (Name.variant_list taken) s in
41199
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   165
                ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   166
                  else Term.all) T
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   167
                 $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   168
                 s' :: taken)
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   169
              end)
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   170
          (Term.add_vars t [] |> sort_wrt (fst o fst))
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   171
  |> fst
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   172
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   173
fun string_for_term ctxt t =
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   174
  Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   175
                   (print_mode_value ())) (Syntax.string_of_term ctxt) t
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   176
  |> String.translate (fn c => if Char.isPrint c then str c else "")
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   177
  |> simplify_spaces
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   178
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   179
(** Structural induction rules **)
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   180
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
   181
fun struct_induct_rule_on th =
41199
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   182
  case Logic.strip_horn (prop_of th) of
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   183
    (prems, @{const Trueprop}
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   184
            $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   185
    if not (is_TVar ind_T) andalso length prems > 1 andalso
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   186
       exists (exists_subterm (curry (op aconv) p)) prems andalso
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   187
       not (exists (exists_subterm (curry (op aconv) a)) prems) then
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   188
      SOME (p_name, ind_T)
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   189
    else
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   190
      NONE
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   191
  | _ => NONE
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   192
43245
cef69d31bfa4 optimized the relevance filter a little bit
blanchet
parents: 43085
diff changeset
   193
fun instantiate_induct_rule ctxt concl_prop p_name ((name, loc), th) ind_x =
41199
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   194
  let
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   195
    fun varify_noninducts (t as Free (s, T)) =
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   196
        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
   197
      | varify_noninducts t = t
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   198
    val p_inst =
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   199
      concl_prop |> map_aterms varify_noninducts |> close_form
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   200
                 |> lambda (Free ind_x)
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   201
                 |> string_for_term ctxt
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   202
  in
41207
f9c7bdc75dd0 reintroduce the higher penalty for skolems
blanchet
parents: 41205
diff changeset
   203
    ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]", loc),
43245
cef69d31bfa4 optimized the relevance filter a little bit
blanchet
parents: 43085
diff changeset
   204
     th |> read_instantiate ctxt [((p_name, 0), p_inst)])
41199
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   205
  end
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   206
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   207
fun type_match thy (T1, T2) =
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   208
  (Sign.typ_match thy (T2, T1) Vartab.empty; true)
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   209
  handle Type.TYPE_MATCH => false
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   210
43245
cef69d31bfa4 optimized the relevance filter a little bit
blanchet
parents: 43085
diff changeset
   211
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
   212
  case struct_induct_rule_on th of
41199
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   213
    SOME (p_name, ind_T) =>
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42358
diff changeset
   214
    let val thy = Proof_Context.theory_of ctxt in
41199
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   215
      stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T))
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   216
              |> map_filter (try (instantiate_induct_rule ctxt stmt p_name ax))
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   217
    end
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   218
  | NONE => [ax]
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   219
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents: 28065
diff changeset
   220
(***************************************************************)
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents: 28065
diff changeset
   221
(* Relevance Filtering                                         *)
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents: 28065
diff changeset
   222
(***************************************************************)
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   223
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   224
(*** constants with types ***)
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   225
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   226
fun order_of_type (Type (@{type_name fun}, [T1, @{typ bool}])) =
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   227
    order_of_type T1 (* cheat: pretend sets are first-order *)
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   228
  | order_of_type (Type (@{type_name fun}, [T1, T2])) =
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   229
    Int.max (order_of_type T1 + 1, order_of_type T2)
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   230
  | 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
   231
  | order_of_type _ = 0
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   232
38823
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   233
(* An abstraction of Isabelle types and first-order terms *)
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   234
datatype pattern = PVar | PApp of string * pattern list
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   235
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
   236
38823
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   237
fun string_for_pattern PVar = "_"
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   238
  | string_for_pattern (PApp (s, ps)) =
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   239
    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
   240
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
   241
fun string_for_ptype (PType (_, ps)) = string_for_patterns ps
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   242
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   243
(*Is the second type an instance of the first one?*)
38824
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
   244
fun match_pattern (PVar, _) = true
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
   245
  | match_pattern (PApp _, PVar) = false
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
   246
  | match_pattern (PApp (s, ps), PApp (t, qs)) =
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
   247
    s = t andalso match_patterns (ps, qs)
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
   248
and match_patterns (_, []) = true
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
   249
  | match_patterns ([], _) = false
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
   250
  | match_patterns (p :: ps, q :: qs) =
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
   251
    match_pattern (p, q) andalso match_patterns (ps, qs)
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   252
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
   253
38823
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   254
(* Is there a unifiable constant? *)
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   255
fun pconst_mem f consts (s, ps) =
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   256
  exists (curry (match_ptype o f) ps)
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   257
         (map snd (filter (curry (op =) s o fst) consts))
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   258
fun pconst_hyper_mem f const_tab (s, ps) =
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   259
  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
   260
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   261
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
   262
  | pattern_for_type (TFree (s, _)) = PApp (s, [])
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   263
  | pattern_for_type (TVar _) = PVar
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   264
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   265
(* 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
   266
fun ptype thy const x =
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   267
  (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
   268
   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
   269
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
   270
  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
   271
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
   272
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   273
fun string_for_hyper_pconst (s, ps) =
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   274
  s ^ "{" ^ commas (map string_for_ptype ps) ^ "}"
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   275
38823
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   276
(* 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
   277
   connective, which we ignore.*)
41066
3890ef4e02f9 pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
blanchet
parents: 40418
diff changeset
   278
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
   279
  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
   280
  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
   281
42741
546b0bda3cb8 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents: 42738
diff changeset
   282
(* Set constants tend to pull in too many irrelevant facts. We limit the damage
546b0bda3cb8 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents: 42738
diff changeset
   283
   by treating them more or less as if they were built-in but add their
546b0bda3cb8 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents: 42738
diff changeset
   284
   definition at the end. *)
546b0bda3cb8 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents: 42738
diff changeset
   285
val set_consts =
546b0bda3cb8 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents: 42738
diff changeset
   286
  [(@{const_name Collect}, @{thms Collect_def}),
546b0bda3cb8 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents: 42738
diff changeset
   287
   (@{const_name Set.member}, @{thms mem_def})]
546b0bda3cb8 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents: 42738
diff changeset
   288
546b0bda3cb8 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents: 42738
diff changeset
   289
val is_set_const = AList.defined (op =) set_consts
546b0bda3cb8 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents: 42738
diff changeset
   290
42732
86683865278d no penality for constants that appear in chained facts
blanchet
parents: 42730
diff changeset
   291
fun add_pconsts_in_term thy is_built_in_const also_skolems pos =
37505
d9af5c01dc4a added code to optionally perform fact filtering on the original (non-CNF) formulas
blanchet
parents: 37504
diff changeset
   292
  let
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
   293
    val flip = Option.map not
38587
1317657d6aa9 fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents: 38395
diff changeset
   294
    (* We include free variables, as well as constants, to handle locales. For
41205
209546e0af2c comment tuning
blanchet
parents: 41204
diff changeset
   295
       each quantifiers that must necessarily be skolemized by the automatic
209546e0af2c comment tuning
blanchet
parents: 41204
diff changeset
   296
       prover, we introduce a fresh constant to simulate the effect of
209546e0af2c comment tuning
blanchet
parents: 41204
diff changeset
   297
       Skolemization. *)
42741
546b0bda3cb8 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents: 42738
diff changeset
   298
    fun do_const const ext_arg (x as (s, _)) ts =
41336
0ea5b9c7d233 proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents: 41279
diff changeset
   299
      let val (built_in, ts) = is_built_in_const x ts in
42741
546b0bda3cb8 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents: 42738
diff changeset
   300
        if is_set_const s then
546b0bda3cb8 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents: 42738
diff changeset
   301
          fold (do_term ext_arg) ts
546b0bda3cb8 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents: 42738
diff changeset
   302
        else
546b0bda3cb8 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents: 42738
diff changeset
   303
          (not built_in
546b0bda3cb8 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents: 42738
diff changeset
   304
           ? add_pconst_to_table also_skolems (rich_pconst thy const x))
546b0bda3cb8 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents: 42738
diff changeset
   305
          #> fold (do_term false) ts
41336
0ea5b9c7d233 proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents: 41279
diff changeset
   306
      end
42741
546b0bda3cb8 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents: 42738
diff changeset
   307
    and do_term ext_arg t =
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   308
      case strip_comb t of
42741
546b0bda3cb8 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents: 42738
diff changeset
   309
        (Const x, ts) => do_const true ext_arg x ts
546b0bda3cb8 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents: 42738
diff changeset
   310
      | (Free x, ts) => do_const false ext_arg x ts
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   311
      | (Abs (_, T, t'), ts) =>
42741
546b0bda3cb8 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents: 42738
diff changeset
   312
        ((null ts andalso not ext_arg)
546b0bda3cb8 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents: 42738
diff changeset
   313
         (* Since lambdas on the right-hand side of equalities are usually
546b0bda3cb8 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents: 42738
diff changeset
   314
            extensionalized later by "extensionalize_term", we don't penalize
546b0bda3cb8 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents: 42738
diff changeset
   315
            them here. *)
41066
3890ef4e02f9 pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
blanchet
parents: 40418
diff changeset
   316
         ? add_pconst_to_table true (abs_name, PType (order_of_type T + 1, [])))
42735
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   317
        #> fold (do_term false) (t' :: ts)
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   318
      | (_, ts) => fold (do_term false) ts
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   319
    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
   320
      do_formula pos body_t
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   321
      #> (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
   322
            add_pconst_to_table true
43559
c1966f322105 old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;
wenzelm
parents: 43492
diff changeset
   323
                (legacy_gensym skolem_prefix, 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
   324
          else
1317657d6aa9 fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents: 38395
diff changeset
   325
            I)
42741
546b0bda3cb8 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents: 42738
diff changeset
   326
    and do_term_or_formula ext_arg T =
546b0bda3cb8 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents: 42738
diff changeset
   327
      if T = HOLogic.boolT then do_formula NONE else do_term ext_arg
37537
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   328
    and do_formula pos t =
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   329
      case t of
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   330
        Const (@{const_name all}, _) $ Abs (_, T, t') =>
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   331
        do_quantifier (pos = SOME false) T t'
37537
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   332
      | @{const "==>"} $ t1 $ t2 =>
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   333
        do_formula (flip pos) t1 #> do_formula pos t2
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   334
      | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
42741
546b0bda3cb8 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents: 42738
diff changeset
   335
        do_term_or_formula false T t1 #> do_term_or_formula true T t2
37537
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   336
      | @{const Trueprop} $ t1 => do_formula pos t1
41140
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   337
      | @{const False} => I
9c68004b8c9d added Sledgehammer support for higher-order propositional reasoning
blanchet
parents: 41138
diff changeset
   338
      | @{const True} => I
37537
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   339
      | @{const Not} $ t1 => do_formula (flip pos) t1
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   340
      | Const (@{const_name All}, _) $ Abs (_, T, t') =>
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   341
        do_quantifier (pos = SOME false) T t'
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   342
      | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   343
        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
   344
      | @{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
   345
      | @{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
   346
      | @{const HOL.implies} $ t1 $ t2 =>
37537
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   347
        do_formula (flip pos) t1 #> do_formula pos t2
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38829
diff changeset
   348
      | Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2 =>
42741
546b0bda3cb8 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents: 42738
diff changeset
   349
        do_term_or_formula false T t1 #> do_term_or_formula true T t2
38587
1317657d6aa9 fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents: 38395
diff changeset
   350
      | 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
   351
        $ t1 $ t2 $ t3 =>
42735
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   352
        do_formula NONE t1 #> fold (do_term_or_formula false T) [t2, t3]
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   353
      | Const (@{const_name Ex1}, _) $ Abs (_, T, t') =>
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   354
        do_quantifier (is_some pos) T t'
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   355
      | Const (@{const_name Ball}, _) $ t1 $ Abs (_, T, t') =>
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   356
        do_quantifier (pos = SOME false) T
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   357
                      (HOLogic.mk_imp (incr_boundvars 1 t1 $ Bound 0, t'))
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   358
      | Const (@{const_name Bex}, _) $ t1 $ Abs (_, T, t') =>
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   359
        do_quantifier (pos = SOME true) T
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   360
                      (HOLogic.mk_conj (incr_boundvars 1 t1 $ Bound 0, t'))
37537
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   361
      | (t0 as Const (_, @{typ bool})) $ t1 =>
42735
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   362
        do_term false t0 #> do_formula pos t1  (* theory constant *)
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   363
      | _ => do_term false t
42732
86683865278d no penality for constants that appear in chained facts
blanchet
parents: 42730
diff changeset
   364
  in do_formula pos end
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   365
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   366
(*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
   367
  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
   368
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
   369
                     : relevance_fudge) thy_name t =
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   370
  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
   371
                                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
   372
    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
   373
  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
   374
    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
   375
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
   376
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
   377
  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
   378
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   379
(**** Constant / Type Frequencies ****)
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   380
38743
69fa75354c58 simplify more code
blanchet
parents: 38742
diff changeset
   381
(* A two-dimensional symbol table counts frequencies of constants. It's keyed
69fa75354c58 simplify more code
blanchet
parents: 38742
diff changeset
   382
   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
   383
   latter, we need a linear ordering on "pattern list". *)
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   384
38823
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   385
fun pattern_ord p =
38743
69fa75354c58 simplify more code
blanchet
parents: 38742
diff changeset
   386
  case p of
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   387
    (PVar, PVar) => EQUAL
38823
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   388
  | (PVar, PApp _) => LESS
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   389
  | (PApp _, PVar) => GREATER
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   390
  | (PApp q1, PApp q2) =>
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   391
    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
   392
fun ptype_ord (PType p, PType q) =
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   393
  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
   394
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   395
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
   396
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
   397
fun count_fact_consts thy fudge =
37503
c2dfa26b9da6 cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents: 37502
diff changeset
   398
  let
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   399
    fun do_const const (s, T) ts =
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   400
      (* 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
   401
      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
   402
      |> Symtab.map_default (s, PType_Tab.empty)
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   403
      #> fold do_term ts
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   404
    and do_term t =
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   405
      case strip_comb t of
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   406
        (Const x, ts) => do_const true x ts
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   407
      | (Free x, ts) => do_const false x ts
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   408
      | (Abs (_, _, t'), ts) => fold do_term (t' :: ts)
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   409
      | (_, ts) => fold do_term ts
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   410
  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
   411
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   412
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   413
(**** Actual Filtering Code ****)
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   414
39367
blanchet
parents: 39366
diff changeset
   415
fun pow_int _ 0 = 1.0
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   416
  | pow_int x 1 = x
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   417
  | 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
   418
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   419
(*The frequency of a constant is the sum of those of all instances of its type.*)
38824
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
   420
fun pconst_freq match const_tab (c, ps) =
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   421
  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
   422
                 (the (Symtab.lookup const_tab c)) 0
38686
45eeee8d6b12 modified relevance filter
blanchet
parents: 38684
diff changeset
   423
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   424
38085
cc44e887246c avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents: 38027
diff changeset
   425
(* 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
   426
   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
   427
c2dfa26b9da6 cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents: 37502
diff changeset
   428
(* "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
   429
   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
   430
   rare ones. *)
39367
blanchet
parents: 39366
diff changeset
   431
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
   432
2b93dbc07778 improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents: 38937
diff changeset
   433
(* 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
   434
   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
   435
   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
   436
   so common as to be of little interest. *)
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   437
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
   438
                      : relevance_fudge) order freq =
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   439
  let val (k, x) = worse_irrel_freq |> `Real.ceil in
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   440
    (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
   441
     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
   442
    * pow_int higher_order_irrel_weight (order - 1)
38938
2b93dbc07778 improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents: 38937
diff changeset
   443
  end
37503
c2dfa26b9da6 cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents: 37502
diff changeset
   444
41790
56dcd46ddf7a give more weight to Frees than to Consts in relevance filter
blanchet
parents: 41768
diff changeset
   445
fun multiplier_for_const_name local_const_multiplier s =
56dcd46ddf7a give more weight to Frees than to Consts in relevance filter
blanchet
parents: 41768
diff changeset
   446
  if String.isSubstring "." s then 1.0 else local_const_multiplier
38821
d0275b6c4e9d avoid needless "that" fact
blanchet
parents: 38820
diff changeset
   447
41790
56dcd46ddf7a give more weight to Frees than to Consts in relevance filter
blanchet
parents: 41768
diff changeset
   448
(* Computes a constant's weight, as determined by its frequency. *)
56dcd46ddf7a give more weight to Frees than to Consts in relevance filter
blanchet
parents: 41768
diff changeset
   449
fun generic_pconst_weight local_const_multiplier abs_weight skolem_weight
42735
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   450
                          theory_const_weight chained_const_weight weight_for f
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   451
                          const_tab chained_const_tab (c as (s, PType (m, _))) =
41790
56dcd46ddf7a give more weight to Frees than to Consts in relevance filter
blanchet
parents: 41768
diff changeset
   452
  if s = abs_name then
56dcd46ddf7a give more weight to Frees than to Consts in relevance filter
blanchet
parents: 41768
diff changeset
   453
    abs_weight
56dcd46ddf7a give more weight to Frees than to Consts in relevance filter
blanchet
parents: 41768
diff changeset
   454
  else if String.isPrefix skolem_prefix s then
56dcd46ddf7a give more weight to Frees than to Consts in relevance filter
blanchet
parents: 41768
diff changeset
   455
    skolem_weight
56dcd46ddf7a give more weight to Frees than to Consts in relevance filter
blanchet
parents: 41768
diff changeset
   456
  else if String.isSuffix theory_const_suffix s then
56dcd46ddf7a give more weight to Frees than to Consts in relevance filter
blanchet
parents: 41768
diff changeset
   457
    theory_const_weight
56dcd46ddf7a give more weight to Frees than to Consts in relevance filter
blanchet
parents: 41768
diff changeset
   458
  else
56dcd46ddf7a give more weight to Frees than to Consts in relevance filter
blanchet
parents: 41768
diff changeset
   459
    multiplier_for_const_name local_const_multiplier s
56dcd46ddf7a give more weight to Frees than to Consts in relevance filter
blanchet
parents: 41768
diff changeset
   460
    * weight_for m (pconst_freq (match_ptype o f) const_tab c)
42735
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   461
    |> (if chained_const_weight < 1.0 andalso
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   462
           pconst_hyper_mem I chained_const_tab c then
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   463
          curry (op *) chained_const_weight
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   464
        else
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   465
          I)
41790
56dcd46ddf7a give more weight to Frees than to Consts in relevance filter
blanchet
parents: 41768
diff changeset
   466
56dcd46ddf7a give more weight to Frees than to Consts in relevance filter
blanchet
parents: 41768
diff changeset
   467
fun rel_pconst_weight ({local_const_multiplier, abs_rel_weight,
56dcd46ddf7a give more weight to Frees than to Consts in relevance filter
blanchet
parents: 41768
diff changeset
   468
                        theory_const_rel_weight, ...} : relevance_fudge)
56dcd46ddf7a give more weight to Frees than to Consts in relevance filter
blanchet
parents: 41768
diff changeset
   469
                      const_tab =
56dcd46ddf7a give more weight to Frees than to Consts in relevance filter
blanchet
parents: 41768
diff changeset
   470
  generic_pconst_weight local_const_multiplier abs_rel_weight 0.0
42735
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   471
                        theory_const_rel_weight 0.0 rel_weight_for I const_tab
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   472
                        Symtab.empty
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   473
41790
56dcd46ddf7a give more weight to Frees than to Consts in relevance filter
blanchet
parents: 41768
diff changeset
   474
fun irrel_pconst_weight (fudge as {local_const_multiplier, abs_irrel_weight,
56dcd46ddf7a give more weight to Frees than to Consts in relevance filter
blanchet
parents: 41768
diff changeset
   475
                                   skolem_irrel_weight,
42735
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   476
                                   theory_const_irrel_weight,
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   477
                                   chained_const_irrel_weight, ...})
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   478
                        const_tab chained_const_tab =
41790
56dcd46ddf7a give more weight to Frees than to Consts in relevance filter
blanchet
parents: 41768
diff changeset
   479
  generic_pconst_weight local_const_multiplier abs_irrel_weight
56dcd46ddf7a give more weight to Frees than to Consts in relevance filter
blanchet
parents: 41768
diff changeset
   480
                        skolem_irrel_weight theory_const_irrel_weight
42735
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   481
                        chained_const_irrel_weight (irrel_weight_for fudge) swap
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   482
                        const_tab chained_const_tab
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   483
43421
926bfe067a32 fixed soundness bug related to extensionality
blanchet
parents: 43351
diff changeset
   484
fun locality_bonus ({intro_bonus, ...} : relevance_fudge) Intro = intro_bonus
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   485
  | locality_bonus {elim_bonus, ...} Elim = elim_bonus
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   486
  | locality_bonus {simp_bonus, ...} Simp = simp_bonus
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   487
  | locality_bonus {local_bonus, ...} Local = local_bonus
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   488
  | locality_bonus {assum_bonus, ...} Assum = assum_bonus
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   489
  | locality_bonus {chained_bonus, ...} Chained = chained_bonus
43421
926bfe067a32 fixed soundness bug related to extensionality
blanchet
parents: 43351
diff changeset
   490
  | locality_bonus _ _ = 0.0
38751
01c4d14b2a61 add a bonus for chained facts, since they are likely to be relevant;
blanchet
parents: 38749
diff changeset
   491
40418
8b73059e97a1 better detection of completely irrelevant facts
blanchet
parents: 40408
diff changeset
   492
fun is_odd_const_name s =
8b73059e97a1 better detection of completely irrelevant facts
blanchet
parents: 40408
diff changeset
   493
  s = abs_name orelse String.isPrefix skolem_prefix s orelse
8b73059e97a1 better detection of completely irrelevant facts
blanchet
parents: 40408
diff changeset
   494
  String.isSuffix theory_const_suffix s
8b73059e97a1 better detection of completely irrelevant facts
blanchet
parents: 40408
diff changeset
   495
42732
86683865278d no penality for constants that appear in chained facts
blanchet
parents: 42730
diff changeset
   496
fun fact_weight fudge loc const_tab relevant_consts chained_consts fact_consts =
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
   497
  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
   498
                   ||> filter_out (pconst_hyper_mem swap relevant_consts) of
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   499
    ([], _) => 0.0
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   500
  | (rel, irrel) =>
40418
8b73059e97a1 better detection of completely irrelevant facts
blanchet
parents: 40408
diff changeset
   501
    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
   502
      0.0
8fe3c26c49af ignore facts with only theory constants in them
blanchet
parents: 40369
diff changeset
   503
    else
8fe3c26c49af ignore facts with only theory constants in them
blanchet
parents: 40369
diff changeset
   504
      let
42735
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   505
        val irrel = irrel |> filter_out (pconst_mem swap rel)
40371
8fe3c26c49af ignore facts with only theory constants in them
blanchet
parents: 40369
diff changeset
   506
        val rel_weight =
8fe3c26c49af ignore facts with only theory constants in them
blanchet
parents: 40369
diff changeset
   507
          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
   508
        val irrel_weight =
8fe3c26c49af ignore facts with only theory constants in them
blanchet
parents: 40369
diff changeset
   509
          ~ (locality_bonus fudge loc)
42735
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   510
          |> fold (curry (op +)
1d375de437e9 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
blanchet
parents: 42732
diff changeset
   511
                   o irrel_pconst_weight fudge const_tab chained_consts) irrel
40371
8fe3c26c49af ignore facts with only theory constants in them
blanchet
parents: 40369
diff changeset
   512
        val res = rel_weight / (rel_weight + irrel_weight)
8fe3c26c49af ignore facts with only theory constants in them
blanchet
parents: 40369
diff changeset
   513
      in if Real.isFinite res then res else 0.0 end
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   514
40369
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40251
diff changeset
   515
fun pconsts_in_fact thy is_built_in_const t =
38825
4ec3cbd95f25 rename and simplify
blanchet
parents: 38824
diff changeset
   516
  Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
42732
86683865278d no penality for constants that appear in chained facts
blanchet
parents: 42730
diff changeset
   517
              (Symtab.empty |> add_pconsts_in_term thy is_built_in_const true
86683865278d no penality for constants that appear in chained facts
blanchet
parents: 42730
diff changeset
   518
                                                   (SOME true) t) []
42729
e011f632227c tune whitespace
blanchet
parents: 42728
diff changeset
   519
40369
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40251
diff changeset
   520
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
   521
  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
   522
            |> pconsts_in_fact thy is_built_in_const of
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   523
    [] => 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
   524
  | consts => SOME ((fact, consts), NONE)
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   525
41768
dd2125fb75f9 export more functionality of Sledgehammer to applications (for experiments)
blanchet
parents: 41767
diff changeset
   526
val const_names_in_fact = map fst ooo pconsts_in_fact
dd2125fb75f9 export more functionality of Sledgehammer to applications (for experiments)
blanchet
parents: 41767
diff changeset
   527
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   528
type annotated_thm =
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   529
  (((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
   530
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42641
diff changeset
   531
fun take_most_relevant ctxt max_relevant remaining_max
42728
44cd74a419ce added configuration options for experimental features
blanchet
parents: 42702
diff changeset
   532
        ({max_imperfect, max_imperfect_exp, ...} : relevance_fudge)
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   533
        (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
   534
  let
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   535
    val max_imperfect =
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   536
      Real.ceil (Math.pow (max_imperfect,
38904
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   537
                    Math.pow (Real.fromInt remaining_max
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   538
                              / Real.fromInt max_relevant, max_imperfect_exp)))
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   539
    val (perfect, imperfect) =
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   540
      candidates |> sort (Real.compare o swap o pairself snd)
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   541
                 |> take_prefix (fn (_, w) => w > 0.99999)
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   542
    val ((accepts, more_rejects), rejects) =
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   543
      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
   544
  in
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42641
diff changeset
   545
    trace_msg ctxt (fn () =>
41491
a2ad5b824051 eliminated Int.toString;
wenzelm
parents: 41336
diff changeset
   546
        "Actually passed (" ^ string_of_int (length accepts) ^ " of " ^
a2ad5b824051 eliminated Int.toString;
wenzelm
parents: 41336
diff changeset
   547
        string_of_int (length candidates) ^ "): " ^
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   548
        (accepts |> map (fn ((((name, _), _), _), weight) =>
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   549
                            name () ^ " [" ^ Real.toString weight ^ "]")
38745
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   550
                 |> commas));
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   551
    (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
   552
  end
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   553
40369
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40251
diff changeset
   554
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
   555
  if Symtab.is_empty tab then
42732
86683865278d no penality for constants that appear in chained facts
blanchet
parents: 42730
diff changeset
   556
    Symtab.empty
86683865278d no penality for constants that appear in chained facts
blanchet
parents: 42730
diff changeset
   557
    |> fold (add_pconsts_in_term thy is_built_in_const false (SOME false))
86683865278d no penality for constants that appear in chained facts
blanchet
parents: 42730
diff changeset
   558
            (map_filter (fn ((_, loc'), th) =>
86683865278d no penality for constants that appear in chained facts
blanchet
parents: 42730
diff changeset
   559
                            if loc' = loc then SOME (prop_of th) else NONE)
86683865278d no penality for constants that appear in chained facts
blanchet
parents: 42730
diff changeset
   560
                        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
   561
  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
   562
    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
   563
42702
blanchet
parents: 42680
diff changeset
   564
fun consider_arities is_built_in_const th =
41158
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   565
  let
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   566
    fun aux _ _ NONE = NONE
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   567
      | aux t args (SOME tab) =
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   568
        case t of
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   569
          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
   570
        | Const (x as (s, _)) =>
41336
0ea5b9c7d233 proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents: 41279
diff changeset
   571
          (if is_built_in_const x args |> fst then
41158
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   572
             SOME tab
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   573
           else case Symtab.lookup tab s of
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   574
             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
   575
           | 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
   576
        | _ => SOME tab
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   577
  in aux (prop_of th) [] end
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   578
42702
blanchet
parents: 42680
diff changeset
   579
(* FIXME: This is currently only useful for polymorphic type systems. *)
blanchet
parents: 42680
diff changeset
   580
fun could_benefit_from_ext is_built_in_const facts =
blanchet
parents: 42680
diff changeset
   581
  fold (consider_arities is_built_in_const o snd) facts (SOME Symtab.empty)
41158
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   582
  |> is_none
8c9c31a757f5 make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents: 41140
diff changeset
   583
43492
43326cadc31a insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents: 43477
diff changeset
   584
(* High enough so that it isn't wrongly considered as very relevant (e.g., for E
43326cadc31a insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents: 43477
diff changeset
   585
   weights), but low enough so that it is unlikely to be truncated away if few
43326cadc31a insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents: 43477
diff changeset
   586
   facts are included. *)
43326cadc31a insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents: 43477
diff changeset
   587
val special_fact_index = 75
43326cadc31a insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents: 43477
diff changeset
   588
44625
4a1132815a70 more tuning
blanchet
parents: 44586
diff changeset
   589
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
   590
        (fudge as {threshold_divisor, ridiculous_threshold, ...})
42732
86683865278d no penality for constants that appear in chained facts
blanchet
parents: 42730
diff changeset
   591
        ({add, del, ...} : relevance_override) facts chained_ts hyp_ts concl_t =
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   592
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42358
diff changeset
   593
    val thy = Proof_Context.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
   594
    val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty
42732
86683865278d no penality for constants that appear in chained facts
blanchet
parents: 42730
diff changeset
   595
    val add_pconsts = add_pconsts_in_term thy is_built_in_const false o SOME
86683865278d no penality for constants that appear in chained facts
blanchet
parents: 42730
diff changeset
   596
    val chained_const_tab = Symtab.empty |> fold (add_pconsts true) chained_ts
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
   597
    val goal_const_tab =
42732
86683865278d no penality for constants that appear in chained facts
blanchet
parents: 42730
diff changeset
   598
      Symtab.empty |> fold (add_pconsts true) hyp_ts
86683865278d no penality for constants that appear in chained facts
blanchet
parents: 42730
diff changeset
   599
                   |> add_pconsts false concl_t
86683865278d no penality for constants that appear in chained facts
blanchet
parents: 42730
diff changeset
   600
      |> (fn tab => if Symtab.is_empty tab then chained_const_tab else tab)
40369
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40251
diff changeset
   601
      |> 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
   602
              [Chained, Assum, Local]
39012
96d97d1c676f cosmetics
blanchet
parents: 38997
diff changeset
   603
    val add_ths = Attrib.eval_thms ctxt add
96d97d1c676f cosmetics
blanchet
parents: 38997
diff changeset
   604
    val del_ths = Attrib.eval_thms ctxt del
42957
c693f9b7674a use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things
blanchet
parents: 42952
diff changeset
   605
    val facts = facts |> filter_out (member Thm.eq_thm_prop del_ths o snd)
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   606
    fun iter j remaining_max threshold rel_const_tab hopeless hopeful =
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   607
      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
   608
        fun relevant [] _ [] =
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   609
            (* Nothing has been added this iteration. *)
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   610
            if j = 0 andalso threshold >= ridiculous_threshold then
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   611
              (* First iteration? Try again. *)
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 39958
diff changeset
   612
              iter 0 max_relevant (threshold / threshold_divisor) rel_const_tab
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   613
                   hopeless hopeful
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   614
            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
   615
              []
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   616
          | relevant candidates rejects [] =
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   617
            let
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   618
              val (accepts, more_rejects) =
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42641
diff changeset
   619
                take_most_relevant ctxt max_relevant remaining_max fudge
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42641
diff changeset
   620
                                   candidates
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   621
              val rel_const_tab' =
38745
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   622
                rel_const_tab
41066
3890ef4e02f9 pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
blanchet
parents: 40418
diff changeset
   623
                |> 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
   624
              fun is_dirty (c, _) =
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   625
                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
   626
              val (hopeful_rejects, hopeless_rejects) =
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   627
                 (rejects @ hopeless, ([], []))
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   628
                 |-> fold (fn (ax as (_, consts), old_weight) =>
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   629
                              if exists is_dirty consts then
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   630
                                apfst (cons (ax, NONE))
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   631
                              else
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   632
                                apsnd (cons (ax, old_weight)))
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   633
                 |>> append (more_rejects
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   634
                             |> map (fn (ax as (_, consts), old_weight) =>
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   635
                                        (ax, if exists is_dirty consts then NONE
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   636
                                             else SOME old_weight)))
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   637
              val threshold =
38822
aa0101e618e2 fix threshold computation + remove "op =" from relevant constants
blanchet
parents: 38821
diff changeset
   638
                1.0 - (1.0 - threshold)
aa0101e618e2 fix threshold computation + remove "op =" from relevant constants
blanchet
parents: 38821
diff changeset
   639
                      * Math.pow (decay, Real.fromInt (length accepts))
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   640
              val remaining_max = remaining_max - length accepts
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   641
            in
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42641
diff changeset
   642
              trace_msg ctxt (fn () => "New or updated constants: " ^
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   643
                  commas (rel_const_tab' |> Symtab.dest
38822
aa0101e618e2 fix threshold computation + remove "op =" from relevant constants
blanchet
parents: 38821
diff changeset
   644
                          |> subtract (op =) (rel_const_tab |> Symtab.dest)
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   645
                          |> map string_for_hyper_pconst));
38745
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   646
              map (fst o fst) accepts @
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   647
              (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
   648
                 []
38745
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   649
               else
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   650
                 iter (j + 1) remaining_max threshold rel_const_tab'
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   651
                      hopeless_rejects hopeful_rejects)
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   652
            end
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   653
          | 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
   654
                     (((ax as (((_, loc), _), fact_consts)), cached_weight)
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   655
                      :: hopeful) =
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   656
            let
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   657
              val weight =
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   658
                case cached_weight of
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   659
                  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
   660
                | NONE => fact_weight fudge loc const_tab rel_const_tab
42732
86683865278d no penality for constants that appear in chained facts
blanchet
parents: 42730
diff changeset
   661
                                      chained_const_tab fact_consts
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   662
            in
38741
7635bf8918a1 get rid of "defs_relevant" feature;
blanchet
parents: 38739
diff changeset
   663
              if weight >= threshold then
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   664
                relevant ((ax, weight) :: candidates) rejects hopeful
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   665
              else
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   666
                relevant candidates ((ax, weight) :: rejects) hopeful
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   667
            end
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   668
        in
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42641
diff changeset
   669
          trace_msg ctxt (fn () =>
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   670
              "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
   671
              Real.toString threshold ^ ", constants: " ^
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   672
              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
   673
                      |> filter (curry (op <>) [] o snd)
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   674
                      |> map string_for_hyper_pconst));
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   675
          relevant [] [] hopeful
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   676
        end
42826
be0e66ccebfa append special boring facts rather than prepend them, to avoid confusing E's weighting mechanism
blanchet
parents: 42812
diff changeset
   677
    fun prepend_facts ths accepts =
42957
c693f9b7674a use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things
blanchet
parents: 42952
diff changeset
   678
      ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
c693f9b7674a use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things
blanchet
parents: 42952
diff changeset
   679
       (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
40408
0d0acdf068b8 always honor the max relevant constraint
blanchet
parents: 40375
diff changeset
   680
      |> take max_relevant
42741
546b0bda3cb8 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents: 42738
diff changeset
   681
    fun uses_const s t =
546b0bda3cb8 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents: 42738
diff changeset
   682
      fold_aterms (curry (fn (Const (s', _), false) => s' = s | (_, b) => b)) t
546b0bda3cb8 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
blanchet
parents: 42738
diff changeset
   683
                  false
43066
e0d4841c5b4a fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other
blanchet
parents: 42957
diff changeset
   684
    fun add_set_const_thms accepts (s, ths) =
e0d4841c5b4a fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other
blanchet
parents: 42957
diff changeset
   685
      if exists (uses_const s o prop_of o snd) accepts orelse
e0d4841c5b4a fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other
blanchet
parents: 42957
diff changeset
   686
         exists (uses_const s) (concl_t :: hyp_ts) then
e0d4841c5b4a fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other
blanchet
parents: 42957
diff changeset
   687
        append ths
e0d4841c5b4a fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other
blanchet
parents: 42957
diff changeset
   688
      else
e0d4841c5b4a fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other
blanchet
parents: 42957
diff changeset
   689
        I
43492
43326cadc31a insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents: 43477
diff changeset
   690
    fun insert_into_facts accepts [] = accepts
43326cadc31a insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents: 43477
diff changeset
   691
      | insert_into_facts accepts ths =
43326cadc31a insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents: 43477
diff changeset
   692
        let
43326cadc31a insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents: 43477
diff changeset
   693
          val add = facts |> filter (member Thm.eq_thm_prop ths o snd)
43326cadc31a insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents: 43477
diff changeset
   694
          val (bef, after) =
43326cadc31a insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents: 43477
diff changeset
   695
            accepts |> filter_out (member Thm.eq_thm_prop ths o snd)
43326cadc31a insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents: 43477
diff changeset
   696
                    |> take (max_relevant - length add)
43326cadc31a insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents: 43477
diff changeset
   697
                    |> chop special_fact_index
43326cadc31a insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents: 43477
diff changeset
   698
        in bef @ add @ after end
43326cadc31a insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents: 43477
diff changeset
   699
    fun insert_special_facts accepts =
43066
e0d4841c5b4a fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other
blanchet
parents: 42957
diff changeset
   700
       [] |> could_benefit_from_ext is_built_in_const accepts ? cons @{thm ext}
e0d4841c5b4a fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other
blanchet
parents: 42957
diff changeset
   701
          |> fold (add_set_const_thms accepts) set_consts
43492
43326cadc31a insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents: 43477
diff changeset
   702
          |> insert_into_facts accepts
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   703
  in
40369
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40251
diff changeset
   704
    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
   705
          |> iter 0 max_relevant threshold0 goal_const_tab []
42826
be0e66ccebfa append special boring facts rather than prepend them, to avoid confusing E's weighting mechanism
blanchet
parents: 42812
diff changeset
   706
          |> not (null add_ths) ? prepend_facts add_ths
43492
43326cadc31a insert rather than append special facts to make it less likely that they're truncated away
blanchet
parents: 43477
diff changeset
   707
          |> insert_special_facts
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42641
diff changeset
   708
          |> tap (fn accepts => trace_msg ctxt (fn () =>
41491
a2ad5b824051 eliminated Int.toString;
wenzelm
parents: 41336
diff changeset
   709
                      "Total relevant: " ^ string_of_int (length accepts)))
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   710
  end
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   711
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   712
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   713
(***************************************************************)
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   714
(* Retrieving and filtering lemmas                             *)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   715
(***************************************************************)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   716
33022
c95102496490 Removal of the unused atpset concept, the atp attribute and some related code.
paulson
parents: 32994
diff changeset
   717
(*** retrieve lemmas and filter them ***)
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   718
20757
fe84fe0dfd30 Definitions produced by packages are now blacklisted.
paulson
parents: 20661
diff changeset
   719
(*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
   720
  "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
   721
fun is_package_def a =
40205
277508b07418 if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents: 40204
diff changeset
   722
  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
   723
    (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
   724
     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
   725
  end
20757
fe84fe0dfd30 Definitions produced by packages are now blacklisted.
paulson
parents: 20661
diff changeset
   726
43245
cef69d31bfa4 optimized the relevance filter a little bit
blanchet
parents: 43085
diff changeset
   727
fun uniquify xs =
cef69d31bfa4 optimized the relevance filter a little bit
blanchet
parents: 43085
diff changeset
   728
  Termtab.fold (cons o snd)
cef69d31bfa4 optimized the relevance filter a little bit
blanchet
parents: 43085
diff changeset
   729
               (fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty) []
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   730
37626
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   731
(* FIXME: put other record thms here, or declare as "no_atp" *)
44585
cfe7f4a68e51 added generation of induction rules
nik
parents: 44462
diff changeset
   732
fun multi_base_blacklist ctxt ho_atp =
41199
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   733
  ["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   734
   "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   735
   "weak_case_cong"]
44585
cfe7f4a68e51 added generation of induction rules
nik
parents: 44462
diff changeset
   736
  |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ?
cfe7f4a68e51 added generation of induction rules
nik
parents: 44462
diff changeset
   737
        append ["induct", "inducts"]
38682
3a203da3f89b weed out junk in relevance filter
blanchet
parents: 38681
diff changeset
   738
  |> map (prefix ".")
37626
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   739
44585
cfe7f4a68e51 added generation of induction rules
nik
parents: 44462
diff changeset
   740
val max_lambda_nesting = 3 (*only applies if not ho_atp*)
37626
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   741
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   742
fun term_has_too_many_lambdas max (t1 $ t2) =
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   743
    exists (term_has_too_many_lambdas max) [t1, t2]
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   744
  | term_has_too_many_lambdas max (Abs (_, _, t)) =
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   745
    max = 0 orelse term_has_too_many_lambdas (max - 1) t
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   746
  | term_has_too_many_lambdas _ _ = false
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   747
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   748
(* 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
   749
   quantifiers. *)
44585
cfe7f4a68e51 added generation of induction rules
nik
parents: 44462
diff changeset
   750
fun formula_has_too_many_lambdas true _ _ = false (*i.e. ho_atp*)
cfe7f4a68e51 added generation of induction rules
nik
parents: 44462
diff changeset
   751
  | formula_has_too_many_lambdas _ Ts (Abs (_, T, t)) =
cfe7f4a68e51 added generation of induction rules
nik
parents: 44462
diff changeset
   752
      formula_has_too_many_lambdas false (T :: Ts) t
cfe7f4a68e51 added generation of induction rules
nik
parents: 44462
diff changeset
   753
  | formula_has_too_many_lambdas _ Ts t =
41273
35ce17cd7967 made the relevance filter treat unatomizable facts like "atomize_all" properly (these result in problems that get E spinning seemingly forever);
blanchet
parents: 41211
diff changeset
   754
    if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then
44585
cfe7f4a68e51 added generation of induction rules
nik
parents: 44462
diff changeset
   755
      exists (formula_has_too_many_lambdas false Ts) (#2 (strip_comb t))
37626
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   756
    else
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   757
      term_has_too_many_lambdas max_lambda_nesting t
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   758
38692
89d3550d8e16 cosmetics
blanchet
parents: 38689
diff changeset
   759
(* 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
   760
   was 11. *)
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   761
val max_apply_depth = 15
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   762
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   763
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
   764
  | apply_depth (Abs (_, _, t)) = apply_depth t
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   765
  | apply_depth _ = 0
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   766
44585
cfe7f4a68e51 added generation of induction rules
nik
parents: 44462
diff changeset
   767
fun is_formula_too_complex ho_atp t =
cfe7f4a68e51 added generation of induction rules
nik
parents: 44462
diff changeset
   768
  apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas ho_atp [] t
37626
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   769
39946
78faa9b31202 move Metis into Plain
blanchet
parents: 39896
diff changeset
   770
(* FIXME: Extend to "Meson" and "Metis" *)
37543
2e733b0a963c a76ace919f1c wasn't quite right; second try
blanchet
parents: 37538
diff changeset
   771
val exists_sledgehammer_const =
37626
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   772
  exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   773
38904
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   774
(* FIXME: make more reliable *)
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   775
val exists_low_level_class_const =
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   776
  exists_Const (fn (s, _) =>
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   777
     String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s)
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   778
38821
d0275b6c4e9d avoid needless "that" fact
blanchet
parents: 38820
diff changeset
   779
fun is_metastrange_theorem th =
37626
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   780
  case head_of (concl_of th) of
43576
ebeda6275027 don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents: 43492
diff changeset
   781
    Const (s, _) => (s <> @{const_name Trueprop} andalso
ebeda6275027 don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents: 43492
diff changeset
   782
                     s <> @{const_name "=="})
ebeda6275027 don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents: 43492
diff changeset
   783
  | _ => false
37626
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   784
38821
d0275b6c4e9d avoid needless "that" fact
blanchet
parents: 38820
diff changeset
   785
fun is_that_fact th =
d0275b6c4e9d avoid needless "that" fact
blanchet
parents: 38820
diff changeset
   786
  String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th)
d0275b6c4e9d avoid needless "that" fact
blanchet
parents: 38820
diff changeset
   787
  andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
d0275b6c4e9d avoid needless "that" fact
blanchet
parents: 38820
diff changeset
   788
                           | _ => false) (prop_of th)
d0275b6c4e9d avoid needless "that" fact
blanchet
parents: 38820
diff changeset
   789
37626
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   790
val type_has_top_sort =
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   791
  exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   792
38085
cc44e887246c avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents: 38027
diff changeset
   793
(**** 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
   794
      unsoundness) ****)
21470
7c1b59ddcd56 Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents: 21431
diff changeset
   795
44585
cfe7f4a68e51 added generation of induction rules
nik
parents: 44462
diff changeset
   796
fun is_theorem_bad_for_atps ho_atp exporter thm =
43576
ebeda6275027 don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents: 43492
diff changeset
   797
  is_metastrange_theorem thm orelse
ebeda6275027 don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents: 43492
diff changeset
   798
  (not exporter andalso
ebeda6275027 don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents: 43492
diff changeset
   799
   let val t = prop_of thm in
44585
cfe7f4a68e51 added generation of induction rules
nik
parents: 44462
diff changeset
   800
     is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse
43576
ebeda6275027 don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents: 43492
diff changeset
   801
     exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
ebeda6275027 don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents: 43492
diff changeset
   802
     is_that_fact thm
ebeda6275027 don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents: 43492
diff changeset
   803
   end)
38627
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   804
42641
2cd4e6463842 recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents: 42638
diff changeset
   805
fun meta_equify (@{const Trueprop}
2cd4e6463842 recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents: 42638
diff changeset
   806
                 $ (Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2)) =
2cd4e6463842 recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents: 42638
diff changeset
   807
    Const (@{const_name "=="}, T --> T --> @{typ prop}) $ t1 $ t2
2cd4e6463842 recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents: 42638
diff changeset
   808
  | meta_equify t = t
2cd4e6463842 recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents: 42638
diff changeset
   809
2cd4e6463842 recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents: 42638
diff changeset
   810
val normalize_simp_prop =
2cd4e6463842 recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents: 42638
diff changeset
   811
  meta_equify
2cd4e6463842 recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents: 42638
diff changeset
   812
  #> map_aterms (fn Var ((s, _), T) => Var ((s, 0), T) | t => t)
2cd4e6463842 recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents: 42638
diff changeset
   813
  #> map_types (map_type_tvar (fn ((s, _), S) => TVar ((s, 0), S)))
2cd4e6463842 recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents: 42638
diff changeset
   814
43245
cef69d31bfa4 optimized the relevance filter a little bit
blanchet
parents: 43085
diff changeset
   815
fun clasimpset_rule_table_of ctxt =
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
   816
  let
43245
cef69d31bfa4 optimized the relevance filter a little bit
blanchet
parents: 43085
diff changeset
   817
    fun add loc g f = fold (Termtab.update o rpair loc o g o prop_of o f)
42812
dda4aef7cba4 tuned signature;
wenzelm
parents: 42810
diff changeset
   818
    val {safeIs, safeEs, hazIs, hazEs, ...} = ctxt |> claset_of |> Classical.rep_cs
42810
2425068fe13a slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents: 42741
diff changeset
   819
    val intros = Item_Net.content safeIs @ Item_Net.content hazIs
2425068fe13a slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
wenzelm
parents: 42741
diff changeset
   820
    val elims = map Classical.classical_rule (Item_Net.content safeEs @ Item_Net.content hazEs)
42641
2cd4e6463842 recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents: 42638
diff changeset
   821
    val simps = ctxt |> simpset_of |> dest_ss |> #simps
2cd4e6463842 recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents: 42638
diff changeset
   822
  in
43245
cef69d31bfa4 optimized the relevance filter a little bit
blanchet
parents: 43085
diff changeset
   823
    Termtab.empty |> add Intro I I intros
cef69d31bfa4 optimized the relevance filter a little bit
blanchet
parents: 43085
diff changeset
   824
                  |> add Elim I I elims
cef69d31bfa4 optimized the relevance filter a little bit
blanchet
parents: 43085
diff changeset
   825
                  |> add Simp I snd simps
cef69d31bfa4 optimized the relevance filter a little bit
blanchet
parents: 43085
diff changeset
   826
                  |> add Simp normalize_simp_prop snd simps
42641
2cd4e6463842 recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents: 42638
diff changeset
   827
  end
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
   828
44585
cfe7f4a68e51 added generation of induction rules
nik
parents: 44462
diff changeset
   829
fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths =
38627
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   830
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42358
diff changeset
   831
    val thy = Proof_Context.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
   832
    val global_facts = Global_Theory.facts_of thy
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42358
diff changeset
   833
    val local_facts = Proof_Context.facts_of ctxt
38644
25bbbaf7ce65 don't penalize abstractions in relevance filter + support nameless `foo`-style facts
blanchet
parents: 38629
diff changeset
   834
    val named_locals = local_facts |> Facts.dest_static []
38993
504b9e1efd33 give priority to assumptions in structured proofs
blanchet
parents: 38992
diff changeset
   835
    val assms = Assumption.all_assms_of ctxt
504b9e1efd33 give priority to assumptions in structured proofs
blanchet
parents: 38992
diff changeset
   836
    fun is_assum th = exists (fn ct => prop_of th aconv term_of ct) assms
42957
c693f9b7674a use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things
blanchet
parents: 42952
diff changeset
   837
    val is_chained = member Thm.eq_thm_prop chained_ths
43245
cef69d31bfa4 optimized the relevance filter a little bit
blanchet
parents: 43085
diff changeset
   838
    val clasimpset_table = clasimpset_rule_table_of ctxt
44585
cfe7f4a68e51 added generation of induction rules
nik
parents: 44462
diff changeset
   839
    fun locality_of_theorem global (name: string) th =
44586
eeba1eedf32d improved handling of induction rules in Sledgehammer
nik
parents: 44585
diff changeset
   840
      if String.isSubstring ".induct" name orelse(*FIXME: use structured name*)
eeba1eedf32d improved handling of induction rules in Sledgehammer
nik
parents: 44585
diff changeset
   841
         String.isSubstring ".inducts" name then
44585
cfe7f4a68e51 added generation of induction rules
nik
parents: 44462
diff changeset
   842
           Induction
cfe7f4a68e51 added generation of induction rules
nik
parents: 44462
diff changeset
   843
      else if is_chained th then
42641
2cd4e6463842 recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents: 42638
diff changeset
   844
        Chained
2cd4e6463842 recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents: 42638
diff changeset
   845
      else if global then
43421
926bfe067a32 fixed soundness bug related to extensionality
blanchet
parents: 43351
diff changeset
   846
        case Termtab.lookup clasimpset_table (prop_of th) of
926bfe067a32 fixed soundness bug related to extensionality
blanchet
parents: 43351
diff changeset
   847
          SOME loc => loc
926bfe067a32 fixed soundness bug related to extensionality
blanchet
parents: 43351
diff changeset
   848
        | NONE => if Thm.eq_thm_prop (th, @{thm ext}) then Extensionality
926bfe067a32 fixed soundness bug related to extensionality
blanchet
parents: 43351
diff changeset
   849
                  else General
44585
cfe7f4a68e51 added generation of induction rules
nik
parents: 44462
diff changeset
   850
      else if is_assum th then Assum else Local
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
   851
    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
   852
      not (Thm.has_name_hint th) andalso
42957
c693f9b7674a use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things
blanchet
parents: 42952
diff changeset
   853
      forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
38644
25bbbaf7ce65 don't penalize abstractions in relevance filter + support nameless `foo`-style facts
blanchet
parents: 38629
diff changeset
   854
    val unnamed_locals =
42957
c693f9b7674a use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things
blanchet
parents: 42952
diff changeset
   855
      union Thm.eq_thm_prop (Facts.props local_facts) chained_ths
38820
d0f98bd81a85 add nameless chained facts to the pool of things known to Sledgehammer
blanchet
parents: 38819
diff changeset
   856
      |> 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
   857
    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
   858
      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
   859
    fun add_facts global foldx facts =
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   860
      foldx (fn (name0, ths) =>
43576
ebeda6275027 don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents: 43492
diff changeset
   861
        if not exporter andalso name0 <> "" andalso
42957
c693f9b7674a use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things
blanchet
parents: 42952
diff changeset
   862
           forall (not o member Thm.eq_thm_prop add_ths) ths andalso
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   863
           (Facts.is_concealed facts name0 orelse
42728
44cd74a419ce added configuration options for experimental features
blanchet
parents: 42702
diff changeset
   864
            (not (Config.get ctxt ignore_no_atp) andalso
44cd74a419ce added configuration options for experimental features
blanchet
parents: 42702
diff changeset
   865
             is_package_def name0) orelse
44cd74a419ce added configuration options for experimental features
blanchet
parents: 42702
diff changeset
   866
            exists (fn s => String.isSuffix s name0)
44585
cfe7f4a68e51 added generation of induction rules
nik
parents: 44462
diff changeset
   867
                   (multi_base_blacklist ctxt ho_atp) orelse
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   868
            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
   869
          I
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   870
        else
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   871
          let
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   872
            val multi = length ths > 1
41279
e0400b05a62c escape backticks in altstrings
blanchet
parents: 41273
diff changeset
   873
            val backquote_thm =
e0400b05a62c escape backticks in altstrings
blanchet
parents: 41273
diff changeset
   874
              backquote o string_for_term ctxt o close_form o prop_of
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   875
            fun check_thms a =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42358
diff changeset
   876
              case try (Proof_Context.get_thms ctxt) a of
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   877
                NONE => false
42957
c693f9b7674a use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things
blanchet
parents: 42952
diff changeset
   878
              | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
38627
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   879
          in
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   880
            pair 1
43245
cef69d31bfa4 optimized the relevance filter a little bit
blanchet
parents: 43085
diff changeset
   881
            #> fold (fn th => fn (j, (multis, unis)) =>
42641
2cd4e6463842 recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents: 42638
diff changeset
   882
                        (j + 1,
43576
ebeda6275027 don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents: 43492
diff changeset
   883
                         if not (member Thm.eq_thm_prop add_ths th) andalso
44585
cfe7f4a68e51 added generation of induction rules
nik
parents: 44462
diff changeset
   884
                            is_theorem_bad_for_atps ho_atp exporter th then
43245
cef69d31bfa4 optimized the relevance filter a little bit
blanchet
parents: 43085
diff changeset
   885
                           (multis, unis)
42641
2cd4e6463842 recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents: 42638
diff changeset
   886
                         else
43245
cef69d31bfa4 optimized the relevance filter a little bit
blanchet
parents: 43085
diff changeset
   887
                           let
cef69d31bfa4 optimized the relevance filter a little bit
blanchet
parents: 43085
diff changeset
   888
                             val new =
cef69d31bfa4 optimized the relevance filter a little bit
blanchet
parents: 43085
diff changeset
   889
                               (((fn () =>
42641
2cd4e6463842 recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents: 42638
diff changeset
   890
                                 if name0 = "" then
2cd4e6463842 recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents: 42638
diff changeset
   891
                                   th |> backquote_thm
2cd4e6463842 recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents: 42638
diff changeset
   892
                                 else
2cd4e6463842 recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents: 42638
diff changeset
   893
                                   [Facts.extern ctxt facts name0,
2cd4e6463842 recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents: 42638
diff changeset
   894
                                    Name_Space.extern ctxt full_space name0,
2cd4e6463842 recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents: 42638
diff changeset
   895
                                    name0]
2cd4e6463842 recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents: 42638
diff changeset
   896
                                   |> find_first check_thms
2cd4e6463842 recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents: 42638
diff changeset
   897
                                   |> (fn SOME name =>
2cd4e6463842 recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents: 42638
diff changeset
   898
                                          make_name reserved multi j name
2cd4e6463842 recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents: 42638
diff changeset
   899
                                        | NONE => "")),
44585
cfe7f4a68e51 added generation of induction rules
nik
parents: 44462
diff changeset
   900
                                locality_of_theorem global name0 th), th)
43245
cef69d31bfa4 optimized the relevance filter a little bit
blanchet
parents: 43085
diff changeset
   901
                           in
cef69d31bfa4 optimized the relevance filter a little bit
blanchet
parents: 43085
diff changeset
   902
                             if multi then (new :: multis, unis)
cef69d31bfa4 optimized the relevance filter a little bit
blanchet
parents: 43085
diff changeset
   903
                             else (multis, new :: unis)
cef69d31bfa4 optimized the relevance filter a little bit
blanchet
parents: 43085
diff changeset
   904
                           end)) ths
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   905
            #> snd
38627
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   906
          end)
38644
25bbbaf7ce65 don't penalize abstractions in relevance filter + support nameless `foo`-style facts
blanchet
parents: 38629
diff changeset
   907
  in
43245
cef69d31bfa4 optimized the relevance filter a little bit
blanchet
parents: 43085
diff changeset
   908
    (* The single-name theorems go after the multiple-name ones, so that single
cef69d31bfa4 optimized the relevance filter a little bit
blanchet
parents: 43085
diff changeset
   909
       names are preferred when both are available. *)
cef69d31bfa4 optimized the relevance filter a little bit
blanchet
parents: 43085
diff changeset
   910
    ([], []) |> add_facts false fold local_facts (unnamed_locals @ named_locals)
cef69d31bfa4 optimized the relevance filter a little bit
blanchet
parents: 43085
diff changeset
   911
             |> add_facts true Facts.fold_static global_facts global_facts
cef69d31bfa4 optimized the relevance filter a little bit
blanchet
parents: 43085
diff changeset
   912
             |> op @
38644
25bbbaf7ce65 don't penalize abstractions in relevance filter + support nameless `foo`-style facts
blanchet
parents: 38629
diff changeset
   913
  end
38627
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   914
41199
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   915
fun external_frees t =
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   916
  [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
4698d12dd860 instantiate induction rules automatically
blanchet
parents: 41167
diff changeset
   917
44585
cfe7f4a68e51 added generation of induction rules
nik
parents: 44462
diff changeset
   918
fun nearly_all_facts ctxt ho_atp ({add, only, ...} : relevance_override)
cfe7f4a68e51 added generation of induction rules
nik
parents: 44462
diff changeset
   919
                     chained_ths hyp_ts concl_t =
43351
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43324
diff changeset
   920
  let
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43324
diff changeset
   921
    val thy = Proof_Context.theory_of ctxt
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43324
diff changeset
   922
    val reserved = reserved_isar_keyword_table ()
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43324
diff changeset
   923
    val add_ths = Attrib.eval_thms ctxt add
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43324
diff changeset
   924
    val ind_stmt =
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43324
diff changeset
   925
      Logic.list_implies (hyp_ts |> filter_out (null o external_frees), concl_t)
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43324
diff changeset
   926
      |> Object_Logic.atomize_term thy
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43324
diff changeset
   927
    val ind_stmt_xs = external_frees ind_stmt
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43324
diff changeset
   928
  in
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43324
diff changeset
   929
    (if only then
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43324
diff changeset
   930
       maps (map (fn ((name, loc), th) => ((K name, loc), th))
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43324
diff changeset
   931
             o fact_from_ref ctxt reserved chained_ths) add
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43324
diff changeset
   932
     else
44585
cfe7f4a68e51 added generation of induction rules
nik
parents: 44462
diff changeset
   933
       all_facts ctxt ho_atp reserved false add_ths chained_ths)
43351
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43324
diff changeset
   934
    |> Config.get ctxt instantiate_inducts
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43324
diff changeset
   935
       ? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43324
diff changeset
   936
    |> (not (Config.get ctxt ignore_no_atp) andalso not only)
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43324
diff changeset
   937
       ? filter_out (No_ATPs.member ctxt o snd)
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43324
diff changeset
   938
    |> uniquify
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43324
diff changeset
   939
  end
b19d95b4d736 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents: 43324
diff changeset
   940
44625
4a1132815a70 more tuning
blanchet
parents: 44586
diff changeset
   941
fun relevant_facts ctxt (threshold0, threshold1) max_relevant is_built_in_const
4a1132815a70 more tuning
blanchet
parents: 44586
diff changeset
   942
                   fudge (override as {only, ...}) chained_ths hyp_ts concl_t
4a1132815a70 more tuning
blanchet
parents: 44586
diff changeset
   943
                   facts =
37538
97ab019d5ac8 make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents: 37537
diff changeset
   944
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42358
diff changeset
   945
    val thy = Proof_Context.theory_of ctxt
38822
aa0101e618e2 fix threshold computation + remove "op =" from relevant constants
blanchet
parents: 38821
diff changeset
   946
    val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
aa0101e618e2 fix threshold computation + remove "op =" from relevant constants
blanchet
parents: 38821
diff changeset
   947
                          1.0 / Real.fromInt (max_relevant + 1))
37538
97ab019d5ac8 make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents: 37537
diff changeset
   948
  in
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42641
diff changeset
   949
    trace_msg ctxt (fn () => "Considering " ^ string_of_int (length facts) ^
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42641
diff changeset
   950
                             " facts");
39366
f58fbb959826 handle relevance filter corner cases more gracefully;
blanchet
parents: 39265
diff changeset
   951
    (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
   952
       facts
39366
f58fbb959826 handle relevance filter corner cases more gracefully;
blanchet
parents: 39265
diff changeset
   953
     else if threshold0 > 1.0 orelse threshold0 > threshold1 orelse
f58fbb959826 handle relevance filter corner cases more gracefully;
blanchet
parents: 39265
diff changeset
   954
             max_relevant = 0 then
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   955
       []
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   956
     else
44625
4a1132815a70 more tuning
blanchet
parents: 44586
diff changeset
   957
       relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
4a1132815a70 more tuning
blanchet
parents: 44586
diff changeset
   958
           fudge override facts (chained_ths |> map prop_of) hyp_ts
4a1132815a70 more tuning
blanchet
parents: 44586
diff changeset
   959
           (concl_t |> theory_constify fudge (Context.theory_name thy)))
38822
aa0101e618e2 fix threshold computation + remove "op =" from relevant constants
blanchet
parents: 38821
diff changeset
   960
    |> 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
   961
  end
30536
07b4f050e4df split relevance-filter and writing of problem-files;
immler@in.tum.de
parents: 30364
diff changeset
   962
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
   963
end;