src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
author blanchet
Wed, 01 Sep 2010 16:46:11 +0200
changeset 38996 6905ba37376c
parent 38994 7c655a491bce
child 38997 78ac4468cf9d
permissions -rw-r--r--
generalize theorem argument parsing syntax
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
33309
5f67433e6dd8 proper header;
wenzelm
parents: 33306
diff changeset
     4
*)
15452
e2a721567f67 Jia Meng: delta simpsets and clasets
paulson
parents: 15347
diff changeset
     5
38988
483879af0643 finished renaming
blanchet
parents: 38986
diff changeset
     6
signature SLEDGEHAMMER_FILTER =
16802
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
     7
sig
38993
504b9e1efd33 give priority to assumptions in structured proofs
blanchet
parents: 38992
diff changeset
     8
  datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
     9
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35963
diff changeset
    10
  type relevance_override =
38996
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
    11
    {add: (Facts.ref * Attrib.src list) list,
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
    12
     del: (Facts.ref * Attrib.src list) list,
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35963
diff changeset
    13
     only: bool}
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35963
diff changeset
    14
37616
c8d2d84d6011 always perform relevance filtering on original formulas
blanchet
parents: 37580
diff changeset
    15
  val trace : bool Unsynchronized.ref
38938
2b93dbc07778 improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents: 38937
diff changeset
    16
  val worse_irrel_freq : real Unsynchronized.ref
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
    17
  val higher_order_irrel_weight : real Unsynchronized.ref
38899
55391ee96614 made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents: 38891
diff changeset
    18
  val abs_rel_weight : real Unsynchronized.ref
55391ee96614 made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents: 38891
diff changeset
    19
  val abs_irrel_weight : real Unsynchronized.ref
55391ee96614 made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents: 38891
diff changeset
    20
  val skolem_irrel_weight : real Unsynchronized.ref
38992
542474156c66 introduce fudge factors to deal with "theory const"
blanchet
parents: 38988
diff changeset
    21
  val theory_const_rel_weight : real Unsynchronized.ref
542474156c66 introduce fudge factors to deal with "theory const"
blanchet
parents: 38988
diff changeset
    22
  val theory_const_irrel_weight : real Unsynchronized.ref
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
    23
  val intro_bonus : real Unsynchronized.ref
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
    24
  val elim_bonus : real Unsynchronized.ref
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
    25
  val simp_bonus : real Unsynchronized.ref
38899
55391ee96614 made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents: 38891
diff changeset
    26
  val local_bonus : real Unsynchronized.ref
38993
504b9e1efd33 give priority to assumptions in structured proofs
blanchet
parents: 38992
diff changeset
    27
  val assum_bonus : real Unsynchronized.ref
38899
55391ee96614 made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents: 38891
diff changeset
    28
  val chained_bonus : real Unsynchronized.ref
38904
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
    29
  val max_imperfect : real Unsynchronized.ref
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
    30
  val max_imperfect_exp : real Unsynchronized.ref
38899
55391ee96614 made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents: 38891
diff changeset
    31
  val threshold_divisor : real Unsynchronized.ref
55391ee96614 made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents: 38891
diff changeset
    32
  val ridiculous_threshold : real Unsynchronized.ref
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
    33
  val name_thm_pairs_from_ref :
38996
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
    34
    Proof.context -> unit Symtab.table -> thm list
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
    35
    -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
37347
635425a442e8 show more respect for user-specified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents: 37345
diff changeset
    36
  val relevant_facts :
38891
6e47e54214b8 remove needless parameter
blanchet
parents: 38889
diff changeset
    37
    Proof.context -> bool -> real * real -> int -> bool -> relevance_override
6e47e54214b8 remove needless parameter
blanchet
parents: 38889
diff changeset
    38
    -> thm list -> term list -> term -> ((string * locality) * thm) list
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    39
end;
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    40
38988
483879af0643 finished renaming
blanchet
parents: 38986
diff changeset
    41
structure Sledgehammer_Filter : SLEDGEHAMMER_FILTER =
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    42
struct
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    43
38652
e063be321438 perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents: 38644
diff changeset
    44
open Sledgehammer_Util
e063be321438 perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents: 38644
diff changeset
    45
37616
c8d2d84d6011 always perform relevance filtering on original formulas
blanchet
parents: 37580
diff changeset
    46
val trace = Unsynchronized.ref false
c8d2d84d6011 always perform relevance filtering on original formulas
blanchet
parents: 37580
diff changeset
    47
fun trace_msg msg = if !trace then tracing (msg ()) else ()
35826
1590abc3d42a renamed Sledgehammer structures
blanchet
parents: 35825
diff changeset
    48
38828
91ad85f962c4 turn off experimental feature per default + avoid exception on "theory constant"
blanchet
parents: 38827
diff changeset
    49
(* experimental feature *)
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
    50
val term_patterns = false
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
    51
37580
c2c1caff5dea got rid of "respect_no_atp" option, which even I don't use
blanchet
parents: 37578
diff changeset
    52
val respect_no_atp = true
37505
d9af5c01dc4a added code to optionally perform fact filtering on the original (non-CNF) formulas
blanchet
parents: 37504
diff changeset
    53
38993
504b9e1efd33 give priority to assumptions in structured proofs
blanchet
parents: 38992
diff changeset
    54
datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
    55
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35963
diff changeset
    56
type relevance_override =
38996
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
    57
  {add: (Facts.ref * Attrib.src list) list,
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
    58
   del: (Facts.ref * Attrib.src list) list,
35966
f8c738abaed8 honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents: 35963
diff changeset
    59
   only: bool}
21070
0a898140fea2 Added more debugging info
paulson
parents: 20995
diff changeset
    60
37616
c8d2d84d6011 always perform relevance filtering on original formulas
blanchet
parents: 37580
diff changeset
    61
val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
38992
542474156c66 introduce fudge factors to deal with "theory const"
blanchet
parents: 38988
diff changeset
    62
val abs_name = "Sledgehammer.abs"
542474156c66 introduce fudge factors to deal with "theory const"
blanchet
parents: 38988
diff changeset
    63
val skolem_prefix = "Sledgehammer.sko"
542474156c66 introduce fudge factors to deal with "theory const"
blanchet
parents: 38988
diff changeset
    64
val theory_const_suffix = Long_Name.separator ^ " 1"
37616
c8d2d84d6011 always perform relevance filtering on original formulas
blanchet
parents: 37580
diff changeset
    65
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
    66
fun repair_name reserved multi j name =
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
    67
  (name |> Symtab.defined reserved name ? quote) ^
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
    68
  (if multi then "(" ^ Int.toString j ^ ")" else "")
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
    69
38996
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
    70
fun name_thm_pairs_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
    71
  let
38996
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
    72
    val ths = Attrib.eval_thms ctxt [xthm]
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
    73
    val bracket =
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
    74
      implode (map (fn arg => "[" ^ Pretty.str_of (Args.pretty_src ctxt arg)
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
    75
                               ^ "]") args)
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
    76
    val space_bracket = if bracket = "" then "" else " " ^ bracket
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
    77
    val name =
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
    78
      case xref of
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
    79
        Facts.Fact s => "`" ^ s ^ "`" ^ space_bracket
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
    80
      | Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
    81
      | _ => Facts.string_of_ref xref ^ space_bracket
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
    82
    val multi = length ths > 1
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
    83
  in
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
    84
    (ths, (1, []))
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
    85
    |-> fold (fn th => fn (j, rest) =>
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
    86
                 (j + 1, ((repair_name reserved multi j name,
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
    87
                          if member Thm.eq_thm chained_ths th then Chained
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
    88
                          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
    89
    |> snd
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
    90
  end
37616
c8d2d84d6011 always perform relevance filtering on original formulas
blanchet
parents: 37580
diff changeset
    91
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents: 28065
diff changeset
    92
(***************************************************************)
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents: 28065
diff changeset
    93
(* Relevance Filtering                                         *)
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents: 28065
diff changeset
    94
(***************************************************************)
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
    95
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
    96
(*** constants with types ***)
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
    97
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
    98
fun order_of_type (Type (@{type_name fun}, [T1, @{typ bool}])) =
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
    99
    order_of_type T1 (* cheat: pretend sets are first-order *)
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   100
  | order_of_type (Type (@{type_name fun}, [T1, T2])) =
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   101
    Int.max (order_of_type T1 + 1, order_of_type T2)
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   102
  | 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
   103
  | order_of_type _ = 0
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   104
38823
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   105
(* An abstraction of Isabelle types and first-order terms *)
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   106
datatype pattern = PVar | PApp of string * pattern list
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   107
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
   108
38823
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   109
fun string_for_pattern PVar = "_"
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   110
  | string_for_pattern (PApp (s, ps)) =
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   111
    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
   112
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
   113
fun string_for_ptype (PType (_, ps)) = string_for_patterns ps
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   114
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   115
(*Is the second type an instance of the first one?*)
38824
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
   116
fun match_pattern (PVar, _) = true
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
   117
  | match_pattern (PApp _, PVar) = false
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
   118
  | match_pattern (PApp (s, ps), PApp (t, qs)) =
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
   119
    s = t andalso match_patterns (ps, qs)
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
   120
and match_patterns (_, []) = true
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
   121
  | match_patterns ([], _) = false
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
   122
  | match_patterns (p :: ps, q :: qs) =
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
   123
    match_pattern (p, q) andalso match_patterns (ps, qs)
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   124
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
   125
38823
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   126
(* Is there a unifiable constant? *)
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   127
fun pconst_mem f consts (s, ps) =
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   128
  exists (curry (match_ptype o f) ps)
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   129
         (map snd (filter (curry (op =) s o fst) consts))
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   130
fun pconst_hyper_mem f const_tab (s, ps) =
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   131
  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
   132
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   133
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
   134
  | pattern_for_type (TFree (s, _)) = PApp (s, [])
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   135
  | pattern_for_type (TVar _) = PVar
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   136
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   137
fun pterm thy t =
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   138
  case strip_comb t of
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   139
    (Const x, ts) => PApp (pconst thy true x ts)
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   140
  | (Free x, ts) => PApp (pconst thy false x ts)
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   141
  | (Var x, []) => PVar
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   142
  | _ => PApp ("?", [])  (* equivalence class of higher-order constructs *)
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   143
(* Pairs a constant with the list of its type instantiations. *)
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   144
and ptype thy const x ts =
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   145
  (if const then map pattern_for_type (these (try (Sign.const_typargs thy) x))
38828
91ad85f962c4 turn off experimental feature per default + avoid exception on "theory constant"
blanchet
parents: 38827
diff changeset
   146
   else []) @
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   147
  (if term_patterns then map (pterm thy) ts else [])
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   148
and pconst thy const (s, T) ts = (s, ptype thy const (s, T) ts)
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   149
and rich_ptype thy const (s, T) ts =
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   150
  PType (order_of_type T, ptype thy const (s, T) ts)
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   151
and rich_pconst thy const (s, T) ts = (s, rich_ptype thy const (s, T) ts)
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   152
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   153
fun string_for_hyper_pconst (s, ps) =
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   154
  s ^ "{" ^ commas (map string_for_ptype ps) ^ "}"
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   155
38822
aa0101e618e2 fix threshold computation + remove "op =" from relevant constants
blanchet
parents: 38821
diff changeset
   156
(* These are typically simplified away by "Meson.presimplify". Equality is
aa0101e618e2 fix threshold computation + remove "op =" from relevant constants
blanchet
parents: 38821
diff changeset
   157
   handled specially via "fequal". *)
38682
3a203da3f89b weed out junk in relevance filter
blanchet
parents: 38681
diff changeset
   158
val boring_consts =
38822
aa0101e618e2 fix threshold computation + remove "op =" from relevant constants
blanchet
parents: 38821
diff changeset
   159
  [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let},
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38829
diff changeset
   160
   @{const_name HOL.eq}]
37537
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   161
38823
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   162
(* 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
   163
   connective, which we ignore.*)
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   164
fun add_pconst_to_table also_skolem (c, 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
   165
  if member (op =) boring_consts c orelse
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
   166
     (not also_skolem andalso String.isPrefix skolem_prefix c) then
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
   167
    I
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
   168
  else
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   169
    Symtab.map_default (c, [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
   170
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
   171
fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
71c9f61516cd if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents: 38818
diff changeset
   172
38906
f76ac80e9bcd fiddle with fact filter
blanchet
parents: 38904
diff changeset
   173
fun pconsts_in_terms thy also_skolems pos ts =
37505
d9af5c01dc4a added code to optionally perform fact filtering on the original (non-CNF) formulas
blanchet
parents: 37504
diff changeset
   174
  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
   175
    val flip = Option.map not
38587
1317657d6aa9 fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents: 38395
diff changeset
   176
    (* We include free variables, as well as constants, to handle locales. For
1317657d6aa9 fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents: 38395
diff changeset
   177
       each quantifiers that must necessarily be skolemized by the ATP, we
1317657d6aa9 fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents: 38395
diff changeset
   178
       introduce a fresh constant to simulate the effect of Skolemization. *)
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   179
    fun do_const const (s, T) ts =
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   180
      add_pconst_to_table also_skolems (rich_pconst thy const (s, T) ts)
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   181
      #> fold do_term ts
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   182
    and do_term t =
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   183
      case strip_comb t of
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   184
        (Const x, ts) => do_const true x ts
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   185
      | (Free x, ts) => do_const false x ts
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   186
      | (Abs (_, T, t'), ts) =>
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   187
        (null ts
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   188
         ? add_pconst_to_table true (abs_name, PType (order_of_type T + 1, [])))
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   189
        #> fold do_term (t' :: ts)
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   190
      | (_, ts) => fold do_term ts
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   191
    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
   192
      do_formula pos body_t
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   193
      #> (if also_skolems andalso will_surely_be_skolemized then
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   194
            add_pconst_to_table true
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   195
                         (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
   196
          else
1317657d6aa9 fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents: 38395
diff changeset
   197
            I)
1317657d6aa9 fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents: 38395
diff changeset
   198
    and do_term_or_formula T =
38692
89d3550d8e16 cosmetics
blanchet
parents: 38689
diff changeset
   199
      if is_formula_type T then do_formula NONE else do_term
37537
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   200
    and do_formula pos t =
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   201
      case t of
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   202
        Const (@{const_name all}, _) $ Abs (_, T, t') =>
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   203
        do_quantifier (pos = SOME false) T t'
37537
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   204
      | @{const "==>"} $ t1 $ t2 =>
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   205
        do_formula (flip pos) t1 #> do_formula pos t2
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   206
      | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
38587
1317657d6aa9 fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents: 38395
diff changeset
   207
        fold (do_term_or_formula T) [t1, t2]
37537
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   208
      | @{const Trueprop} $ t1 => do_formula pos t1
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   209
      | @{const Not} $ t1 => do_formula (flip pos) t1
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   210
      | Const (@{const_name All}, _) $ Abs (_, T, t') =>
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   211
        do_quantifier (pos = SOME false) T t'
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   212
      | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   213
        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
   214
      | @{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
   215
      | @{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
   216
      | @{const HOL.implies} $ t1 $ t2 =>
37537
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   217
        do_formula (flip pos) t1 #> do_formula pos t2
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38829
diff changeset
   218
      | Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2 =>
38587
1317657d6aa9 fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents: 38395
diff changeset
   219
        fold (do_term_or_formula T) [t1, t2]
1317657d6aa9 fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents: 38395
diff changeset
   220
      | 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
   221
        $ t1 $ t2 $ t3 =>
1317657d6aa9 fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents: 38395
diff changeset
   222
        do_formula NONE t1 #> fold (do_term_or_formula T) [t2, t3]
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   223
      | Const (@{const_name Ex1}, _) $ Abs (_, T, t') =>
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   224
        do_quantifier (is_some pos) T t'
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   225
      | Const (@{const_name Ball}, _) $ t1 $ Abs (_, T, t') =>
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   226
        do_quantifier (pos = SOME false) T
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   227
                      (HOLogic.mk_imp (incr_boundvars 1 t1 $ Bound 0, t'))
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   228
      | Const (@{const_name Bex}, _) $ t1 $ Abs (_, T, t') =>
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   229
        do_quantifier (pos = SOME true) T
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   230
                      (HOLogic.mk_conj (incr_boundvars 1 t1 $ Bound 0, t'))
37537
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   231
      | (t0 as Const (_, @{typ bool})) $ t1 =>
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   232
        do_term t0 #> do_formula pos t1  (* theory constant *)
8e56d1ccf189 improve the new "natural formula" fact filter
blanchet
parents: 37515
diff changeset
   233
      | _ => do_term t
38819
71c9f61516cd if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents: 38818
diff changeset
   234
  in Symtab.empty |> fold (do_formula pos) ts end
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   235
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   236
(*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
   237
  takes the given theory into account.*)
37616
c8d2d84d6011 always perform relevance filtering on original formulas
blanchet
parents: 37580
diff changeset
   238
fun theory_const_prop_of theory_relevant th =
37505
d9af5c01dc4a added code to optionally perform fact filtering on the original (non-CNF) formulas
blanchet
parents: 37504
diff changeset
   239
  if theory_relevant then
d9af5c01dc4a added code to optionally perform fact filtering on the original (non-CNF) formulas
blanchet
parents: 37504
diff changeset
   240
    let
d9af5c01dc4a added code to optionally perform fact filtering on the original (non-CNF) formulas
blanchet
parents: 37504
diff changeset
   241
      val name = Context.theory_name (theory_of_thm th)
38992
542474156c66 introduce fudge factors to deal with "theory const"
blanchet
parents: 38988
diff changeset
   242
      val t = Const (name ^ theory_const_suffix, @{typ bool})
37505
d9af5c01dc4a added code to optionally perform fact filtering on the original (non-CNF) formulas
blanchet
parents: 37504
diff changeset
   243
    in t $ prop_of th end
d9af5c01dc4a added code to optionally perform fact filtering on the original (non-CNF) formulas
blanchet
parents: 37504
diff changeset
   244
  else
d9af5c01dc4a added code to optionally perform fact filtering on the original (non-CNF) formulas
blanchet
parents: 37504
diff changeset
   245
    prop_of th
d9af5c01dc4a added code to optionally perform fact filtering on the original (non-CNF) formulas
blanchet
parents: 37504
diff changeset
   246
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   247
(**** Constant / Type Frequencies ****)
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   248
38743
69fa75354c58 simplify more code
blanchet
parents: 38742
diff changeset
   249
(* A two-dimensional symbol table counts frequencies of constants. It's keyed
69fa75354c58 simplify more code
blanchet
parents: 38742
diff changeset
   250
   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
   251
   latter, we need a linear ordering on "pattern list". *)
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   252
38823
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   253
fun pattern_ord p =
38743
69fa75354c58 simplify more code
blanchet
parents: 38742
diff changeset
   254
  case p of
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   255
    (PVar, PVar) => EQUAL
38823
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   256
  | (PVar, PApp _) => LESS
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   257
  | (PApp _, PVar) => GREATER
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   258
  | (PApp q1, PApp q2) =>
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   259
    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
   260
fun ptype_ord (PType p, PType q) =
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   261
  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
   262
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   263
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
   264
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   265
fun count_axiom_consts theory_relevant thy =
37503
c2dfa26b9da6 cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents: 37502
diff changeset
   266
  let
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   267
    fun do_const const (s, T) ts =
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   268
      (* Two-dimensional table update. Constant maps to types maps to count. *)
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   269
      PType_Tab.map_default (rich_ptype thy const (s, T) ts, 0) (Integer.add 1)
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   270
      |> Symtab.map_default (s, PType_Tab.empty)
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   271
      #> fold do_term ts
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   272
    and do_term t =
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   273
      case strip_comb t of
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   274
        (Const x, ts) => do_const true x ts
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   275
      | (Free x, ts) => do_const false x ts
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   276
      | (Abs (_, _, t'), ts) => fold do_term (t' :: ts)
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   277
      | (_, ts) => fold do_term ts
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   278
  in do_term o theory_const_prop_of theory_relevant o snd end
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   279
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   280
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   281
(**** Actual Filtering Code ****)
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   282
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   283
fun pow_int x 0 = 1.0
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   284
  | pow_int x 1 = x
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   285
  | 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
   286
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   287
(*The frequency of a constant is the sum of those of all instances of its type.*)
38824
f74513bbe627 cosmetics
blanchet
parents: 38823
diff changeset
   288
fun pconst_freq match const_tab (c, ps) =
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   289
  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
   290
                 (the (Symtab.lookup const_tab c)) 0
38686
45eeee8d6b12 modified relevance filter
blanchet
parents: 38684
diff changeset
   291
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   292
38085
cc44e887246c avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents: 38027
diff changeset
   293
(* 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
   294
   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
   295
c2dfa26b9da6 cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents: 37502
diff changeset
   296
(* "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
   297
   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
   298
   rare ones. *)
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   299
fun rel_weight_for order 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
   300
2b93dbc07778 improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents: 38937
diff changeset
   301
(* FUDGE *)
2b93dbc07778 improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents: 38937
diff changeset
   302
val worse_irrel_freq = Unsynchronized.ref 100.0
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   303
val higher_order_irrel_weight = Unsynchronized.ref 1.05
38938
2b93dbc07778 improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents: 38937
diff changeset
   304
2b93dbc07778 improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents: 38937
diff changeset
   305
(* 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
   306
   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
   307
   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
   308
   so common as to be of little interest. *)
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   309
fun irrel_weight_for order freq =
38938
2b93dbc07778 improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents: 38937
diff changeset
   310
  let val (k, x) = !worse_irrel_freq |> `Real.ceil in
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   311
    (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
   312
     else rel_weight_for order freq / rel_weight_for order k)
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   313
    * pow_int (!higher_order_irrel_weight) (order - 1)
38938
2b93dbc07778 improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents: 38937
diff changeset
   314
  end
37503
c2dfa26b9da6 cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents: 37502
diff changeset
   315
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   316
(* FUDGE *)
38899
55391ee96614 made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents: 38891
diff changeset
   317
val abs_rel_weight = Unsynchronized.ref 0.5
55391ee96614 made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents: 38891
diff changeset
   318
val abs_irrel_weight = Unsynchronized.ref 2.0
38904
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   319
val skolem_irrel_weight = Unsynchronized.ref 0.75
38992
542474156c66 introduce fudge factors to deal with "theory const"
blanchet
parents: 38988
diff changeset
   320
val theory_const_rel_weight = Unsynchronized.ref 0.5
542474156c66 introduce fudge factors to deal with "theory const"
blanchet
parents: 38988
diff changeset
   321
val theory_const_irrel_weight = Unsynchronized.ref 0.25
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   322
37503
c2dfa26b9da6 cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents: 37502
diff changeset
   323
(* Computes a constant's weight, as determined by its frequency. *)
38992
542474156c66 introduce fudge factors to deal with "theory const"
blanchet
parents: 38988
diff changeset
   324
fun generic_pconst_weight abs_weight skolem_weight theory_const_weight
542474156c66 introduce fudge factors to deal with "theory const"
blanchet
parents: 38988
diff changeset
   325
                          weight_for f const_tab (c as (s, PType (m, _))) =
38816
21a6f261595e lower penalty for Skolem constants
blanchet
parents: 38752
diff changeset
   326
  if s = abs_name then abs_weight
21a6f261595e lower penalty for Skolem constants
blanchet
parents: 38752
diff changeset
   327
  else if String.isPrefix skolem_prefix s then skolem_weight
38992
542474156c66 introduce fudge factors to deal with "theory const"
blanchet
parents: 38988
diff changeset
   328
  else if String.isSuffix theory_const_suffix s then theory_const_weight
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   329
  else weight_for m (pconst_freq (match_ptype o f) const_tab c)
38821
d0275b6c4e9d avoid needless "that" fact
blanchet
parents: 38820
diff changeset
   330
38938
2b93dbc07778 improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents: 38937
diff changeset
   331
fun rel_pconst_weight const_tab =
38992
542474156c66 introduce fudge factors to deal with "theory const"
blanchet
parents: 38988
diff changeset
   332
  generic_pconst_weight (!abs_rel_weight) 0.0 (!theory_const_rel_weight)
542474156c66 introduce fudge factors to deal with "theory const"
blanchet
parents: 38988
diff changeset
   333
                        rel_weight_for I const_tab
38938
2b93dbc07778 improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents: 38937
diff changeset
   334
fun irrel_pconst_weight const_tab =
2b93dbc07778 improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents: 38937
diff changeset
   335
  generic_pconst_weight (!abs_irrel_weight) (!skolem_irrel_weight)
38992
542474156c66 introduce fudge factors to deal with "theory const"
blanchet
parents: 38988
diff changeset
   336
                    (!theory_const_irrel_weight) irrel_weight_for swap const_tab
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   337
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   338
(* FUDGE *)
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
   339
val intro_bonus = Unsynchronized.ref 0.15
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
   340
val elim_bonus = Unsynchronized.ref 0.15
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
   341
val simp_bonus = Unsynchronized.ref 0.15
38906
f76ac80e9bcd fiddle with fact filter
blanchet
parents: 38904
diff changeset
   342
val local_bonus = Unsynchronized.ref 0.55
38994
7c655a491bce fiddled with fudge factor (based on Mirabelle)
blanchet
parents: 38993
diff changeset
   343
val assum_bonus = Unsynchronized.ref 1.05
38901
ee36b983ca22 fiddle with fact filter based on Mirabelle experiments
blanchet
parents: 38899
diff changeset
   344
val chained_bonus = Unsynchronized.ref 1.5
38899
55391ee96614 made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents: 38891
diff changeset
   345
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   346
fun locality_bonus General = 0.0
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
   347
  | locality_bonus Intro = !intro_bonus
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
   348
  | locality_bonus Elim = !elim_bonus
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
   349
  | locality_bonus Simp = !simp_bonus
38899
55391ee96614 made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents: 38891
diff changeset
   350
  | locality_bonus Local = !local_bonus
38993
504b9e1efd33 give priority to assumptions in structured proofs
blanchet
parents: 38992
diff changeset
   351
  | locality_bonus Assum = !assum_bonus
38899
55391ee96614 made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents: 38891
diff changeset
   352
  | locality_bonus Chained = !chained_bonus
38751
01c4d14b2a61 add a bonus for chained facts, since they are likely to be relevant;
blanchet
parents: 38749
diff changeset
   353
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   354
fun axiom_weight loc const_tab relevant_consts axiom_consts =
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   355
  case axiom_consts |> List.partition (pconst_hyper_mem I relevant_consts)
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   356
                    ||> filter_out (pconst_hyper_mem swap relevant_consts) of
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   357
    ([], _) => 0.0
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   358
  | (rel, irrel) =>
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   359
    let
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   360
      val irrel = irrel |> filter_out (pconst_mem swap rel)
38938
2b93dbc07778 improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents: 38937
diff changeset
   361
      val rel_weight =
2b93dbc07778 improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents: 38937
diff changeset
   362
        0.0 |> fold (curry (op +) o rel_pconst_weight const_tab) rel
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   363
      val irrel_weight =
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   364
        ~ (locality_bonus loc)
38938
2b93dbc07778 improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents: 38937
diff changeset
   365
        |> fold (curry (op +) o irrel_pconst_weight const_tab) irrel
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   366
      val res = rel_weight / (rel_weight + irrel_weight)
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   367
    in if Real.isFinite res then res else 0.0 end
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   368
38904
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   369
(* FIXME: experiment
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   370
fun debug_axiom_weight loc const_tab relevant_consts axiom_consts =
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   371
  case axiom_consts |> List.partition (pconst_hyper_mem I relevant_consts)
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   372
                    ||> filter_out (pconst_hyper_mem swap relevant_consts) of
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   373
    ([], _) => 0.0
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   374
  | (rel, irrel) =>
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   375
    let
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   376
      val irrel = irrel |> filter_out (pconst_mem swap rel)
38938
2b93dbc07778 improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents: 38937
diff changeset
   377
      val rels_weight =
2b93dbc07778 improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents: 38937
diff changeset
   378
        0.0 |> fold (curry (op +) o rel_pconst_weight const_tab) rel
2b93dbc07778 improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents: 38937
diff changeset
   379
      val irrels_weight =
38904
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   380
        ~ (locality_bonus loc)
38938
2b93dbc07778 improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents: 38937
diff changeset
   381
        |> fold (curry (op +) o irrel_pconst_weight const_tab) irrel
2b93dbc07778 improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents: 38937
diff changeset
   382
val _ = tracing (PolyML.makestring ("REL: ", map (`(rel_pconst_weight const_tab)) rel))
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   383
val _ = tracing (PolyML.makestring ("IRREL: ", map (`(irrel_pconst_weight const_tab)) irrel))
38938
2b93dbc07778 improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents: 38937
diff changeset
   384
      val res = rels_weight / (rels_weight + irrels_weight)
38904
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   385
    in if Real.isFinite res then res else 0.0 end
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   386
*)
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   387
38823
828e68441a2f renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents: 38822
diff changeset
   388
fun pconsts_in_axiom thy t =
38825
4ec3cbd95f25 rename and simplify
blanchet
parents: 38824
diff changeset
   389
  Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
38906
f76ac80e9bcd fiddle with fact filter
blanchet
parents: 38904
diff changeset
   390
              (pconsts_in_terms thy true (SOME true) [t]) []
38687
97509445c569 cache previous iteration's weights, and keep track of what's dirty and what's clean;
blanchet
parents: 38686
diff changeset
   391
fun pair_consts_axiom theory_relevant thy axiom =
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   392
  case axiom |> snd |> theory_const_prop_of theory_relevant
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   393
             |> pconsts_in_axiom thy of
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   394
    [] => NONE
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   395
  | consts => SOME ((axiom, consts), NONE)
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   396
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   397
type annotated_thm =
38939
f0aa0c49fdbf add a penalty for being higher-order
blanchet
parents: 38938
diff changeset
   398
  (((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
   399
38904
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   400
(* FUDGE *)
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
   401
val max_imperfect = Unsynchronized.ref 11.5
38904
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   402
val max_imperfect_exp = Unsynchronized.ref 1.0
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   403
38904
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   404
fun take_most_relevant max_relevant remaining_max
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   405
                       (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
   406
  let
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   407
    val max_imperfect =
38904
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   408
      Real.ceil (Math.pow (!max_imperfect,
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   409
                    Math.pow (Real.fromInt remaining_max
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   410
                              / Real.fromInt max_relevant, !max_imperfect_exp)))
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   411
    val (perfect, imperfect) =
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   412
      candidates |> sort (Real.compare o swap o pairself snd)
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   413
                 |> take_prefix (fn (_, w) => w > 0.99999)
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   414
    val ((accepts, more_rejects), rejects) =
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   415
      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
   416
  in
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   417
    trace_msg (fn () =>
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   418
        "Actually passed (" ^ Int.toString (length accepts) ^ " of " ^
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   419
        Int.toString (length candidates) ^ "): " ^
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   420
        (accepts |> map (fn ((((name, _), _), _), weight) =>
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   421
                            name () ^ " [" ^ Real.toString weight ^ "]")
38745
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   422
                 |> commas));
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   423
    (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
   424
  end
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   425
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
   426
fun if_empty_replace_with_locality thy axioms loc 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
   427
  if Symtab.is_empty tab then
38906
f76ac80e9bcd fiddle with fact filter
blanchet
parents: 38904
diff changeset
   428
    pconsts_in_terms thy false (SOME false)
38819
71c9f61516cd if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents: 38818
diff changeset
   429
        (map_filter (fn ((_, loc'), th) =>
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
   430
                        if loc' = loc then SOME (prop_of th) else NONE) axioms)
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
   431
  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
   432
    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
   433
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   434
(* FUDGE *)
38899
55391ee96614 made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents: 38891
diff changeset
   435
val threshold_divisor = Unsynchronized.ref 2.0
55391ee96614 made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents: 38891
diff changeset
   436
val ridiculous_threshold = Unsynchronized.ref 0.1
38683
23266607cb81 if no facts were selected on first iteration, try again with a lower threshold
blanchet
parents: 38682
diff changeset
   437
38745
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   438
fun relevance_filter ctxt threshold0 decay max_relevant theory_relevant
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   439
                     ({add, del, ...} : relevance_override) axioms goal_ts =
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   440
  let
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   441
    val thy = ProofContext.theory_of ctxt
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
   442
    val const_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
   443
      fold (count_axiom_consts theory_relevant thy) axioms Symtab.empty
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
   444
    val goal_const_tab =
38906
f76ac80e9bcd fiddle with fact filter
blanchet
parents: 38904
diff changeset
   445
      pconsts_in_terms thy false (SOME false) goal_ts
38993
504b9e1efd33 give priority to assumptions in structured proofs
blanchet
parents: 38992
diff changeset
   446
      |> fold (if_empty_replace_with_locality thy axioms)
504b9e1efd33 give priority to assumptions in structured proofs
blanchet
parents: 38992
diff changeset
   447
              [Chained, Assum, Local]
38996
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
   448
    val add_thms = Attrib.eval_thms ctxt add
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
   449
    val del_thms = Attrib.eval_thms ctxt del
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   450
    fun iter j remaining_max threshold rel_const_tab hopeless hopeful =
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   451
      let
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   452
        fun game_over rejects =
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   453
          (* Add "add:" facts. *)
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   454
          if null add_thms then
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   455
            []
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   456
          else
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   457
            map_filter (fn ((p as (_, th), _), _) =>
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   458
                           if member Thm.eq_thm add_thms th then SOME p
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   459
                           else NONE) rejects
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   460
        fun relevant [] rejects [] =
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   461
            (* Nothing has been added this iteration. *)
38899
55391ee96614 made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents: 38891
diff changeset
   462
            if j = 0 andalso threshold >= !ridiculous_threshold then
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   463
              (* First iteration? Try again. *)
38899
55391ee96614 made all fudge factors in relevance filter references, so that Mirabelle can set them (for experiments)
blanchet
parents: 38891
diff changeset
   464
              iter 0 max_relevant (threshold / !threshold_divisor) rel_const_tab
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   465
                   hopeless hopeful
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   466
            else
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   467
              game_over (rejects @ hopeless)
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   468
          | relevant candidates rejects [] =
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   469
            let
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   470
              val (accepts, more_rejects) =
38904
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   471
                take_most_relevant max_relevant remaining_max candidates
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   472
              val rel_const_tab' =
38745
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   473
                rel_const_tab
38901
ee36b983ca22 fiddle with fact filter based on Mirabelle experiments
blanchet
parents: 38899
diff changeset
   474
                |> 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
   475
              fun is_dirty (c, _) =
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   476
                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
   477
              val (hopeful_rejects, hopeless_rejects) =
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   478
                 (rejects @ hopeless, ([], []))
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   479
                 |-> fold (fn (ax as (_, consts), old_weight) =>
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   480
                              if exists is_dirty consts then
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   481
                                apfst (cons (ax, NONE))
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   482
                              else
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   483
                                apsnd (cons (ax, old_weight)))
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   484
                 |>> append (more_rejects
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   485
                             |> map (fn (ax as (_, consts), old_weight) =>
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   486
                                        (ax, if exists is_dirty consts then NONE
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   487
                                             else SOME old_weight)))
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   488
              val threshold =
38822
aa0101e618e2 fix threshold computation + remove "op =" from relevant constants
blanchet
parents: 38821
diff changeset
   489
                1.0 - (1.0 - threshold)
aa0101e618e2 fix threshold computation + remove "op =" from relevant constants
blanchet
parents: 38821
diff changeset
   490
                      * Math.pow (decay, Real.fromInt (length accepts))
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   491
              val remaining_max = remaining_max - length accepts
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   492
            in
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   493
              trace_msg (fn () => "New or updated constants: " ^
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   494
                  commas (rel_const_tab' |> Symtab.dest
38822
aa0101e618e2 fix threshold computation + remove "op =" from relevant constants
blanchet
parents: 38821
diff changeset
   495
                          |> subtract (op =) (rel_const_tab |> Symtab.dest)
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   496
                          |> map string_for_hyper_pconst));
38745
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   497
              map (fst o fst) accepts @
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   498
              (if remaining_max = 0 then
38745
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   499
                 game_over (hopeful_rejects @ map (apsnd SOME) hopeless_rejects)
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   500
               else
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   501
                 iter (j + 1) remaining_max threshold rel_const_tab'
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   502
                      hopeless_rejects hopeful_rejects)
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   503
            end
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   504
          | relevant candidates rejects
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   505
                     (((ax as (((_, loc), th), axiom_consts)), cached_weight)
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   506
                      :: hopeful) =
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   507
            let
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   508
              val weight =
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   509
                case cached_weight of
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   510
                  SOME w => w
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   511
                | NONE => axiom_weight loc const_tab rel_const_tab axiom_consts
38904
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   512
(* FIXME: experiment
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   513
val name = fst (fst (fst ax)) ()
38938
2b93dbc07778 improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents: 38937
diff changeset
   514
val _ = if String.isSubstring "positive_minus" name orelse String.isSubstring "not_exp_le_zero" name then
38901
ee36b983ca22 fiddle with fact filter based on Mirabelle experiments
blanchet
parents: 38899
diff changeset
   515
tracing ("*** " ^ name ^ PolyML.makestring (debug_axiom_weight loc const_tab rel_const_tab axiom_consts))
38747
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   516
else
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   517
()
b264ae66cede fiddle with relevance filter
blanchet
parents: 38745
diff changeset
   518
*)
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   519
            in
38741
7635bf8918a1 get rid of "defs_relevant" feature;
blanchet
parents: 38739
diff changeset
   520
              if weight >= threshold then
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   521
                relevant ((ax, weight) :: candidates) rejects hopeful
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   522
              else
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   523
                relevant candidates ((ax, weight) :: rejects) hopeful
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   524
            end
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   525
        in
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   526
          trace_msg (fn () =>
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   527
              "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
   528
              Real.toString threshold ^ ", constants: " ^
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   529
              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
   530
                      |> filter (curry (op <>) [] o snd)
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   531
                      |> map string_for_hyper_pconst));
38889
d0e3f68dde63 fiddle with the relevance filter
blanchet
parents: 38829
diff changeset
   532
          relevant [] [] hopeful
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   533
        end
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   534
  in
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   535
    axioms |> filter_out (member Thm.eq_thm del_thms o snd)
38827
cf01645cbbce extended relevance filter with first-order term matching
blanchet
parents: 38825
diff changeset
   536
           |> map_filter (pair_consts_axiom theory_relevant thy)
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
   537
           |> iter 0 max_relevant threshold0 goal_const_tab []
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   538
           |> tap (fn res => trace_msg (fn () =>
38686
45eeee8d6b12 modified relevance filter
blanchet
parents: 38684
diff changeset
   539
                                "Total relevant: " ^ Int.toString (length res)))
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   540
  end
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   541
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   542
24287
c857dac06da6 combining the relevance filter with res_atp
paulson
parents: 24286
diff changeset
   543
(***************************************************************)
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   544
(* Retrieving and filtering lemmas                             *)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   545
(***************************************************************)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   546
33022
c95102496490 Removal of the unused atpset concept, the atp attribute and some related code.
paulson
parents: 32994
diff changeset
   547
(*** retrieve lemmas and filter them ***)
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   548
20757
fe84fe0dfd30 Definitions produced by packages are now blacklisted.
paulson
parents: 20661
diff changeset
   549
(*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
   550
  "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
   551
fun is_package_def a =
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30291
diff changeset
   552
  let val names = Long_Name.explode a
21690
552d20ff9a95 Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents: 21588
diff changeset
   553
  in
552d20ff9a95 Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents: 21588
diff changeset
   554
     length names > 2 andalso
552d20ff9a95 Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents: 21588
diff changeset
   555
     not (hd names = "local") andalso
552d20ff9a95 Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents: 21588
diff changeset
   556
     String.isSuffix "_def" a  orelse  String.isSuffix "_defs" a
552d20ff9a95 Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents: 21588
diff changeset
   557
  end;
20757
fe84fe0dfd30 Definitions produced by packages are now blacklisted.
paulson
parents: 20661
diff changeset
   558
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
   559
fun mk_fact_table f xs =
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   560
  fold (Termtab.update o `(prop_of o f)) xs Termtab.empty
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   561
fun uniquify xs = Termtab.fold (cons o snd) (mk_fact_table snd xs) []
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   562
37626
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   563
(* FIXME: put other record thms here, or declare as "no_atp" *)
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   564
val multi_base_blacklist =
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   565
  ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits",
38682
3a203da3f89b weed out junk in relevance filter
blanchet
parents: 38681
diff changeset
   566
   "split_asm", "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy",
3a203da3f89b weed out junk in relevance filter
blanchet
parents: 38681
diff changeset
   567
   "case_cong", "weak_case_cong"]
3a203da3f89b weed out junk in relevance filter
blanchet
parents: 38681
diff changeset
   568
  |> map (prefix ".")
37626
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   569
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   570
val max_lambda_nesting = 3
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   571
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   572
fun term_has_too_many_lambdas max (t1 $ t2) =
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   573
    exists (term_has_too_many_lambdas max) [t1, t2]
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   574
  | term_has_too_many_lambdas max (Abs (_, _, t)) =
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   575
    max = 0 orelse term_has_too_many_lambdas (max - 1) t
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   576
  | term_has_too_many_lambdas _ _ = false
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   577
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   578
(* 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
   579
   quantifiers. *)
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   580
fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   581
    formula_has_too_many_lambdas (T :: Ts) t
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   582
  | formula_has_too_many_lambdas Ts t =
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   583
    if is_formula_type (fastype_of1 (Ts, t)) then
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   584
      exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   585
    else
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   586
      term_has_too_many_lambdas max_lambda_nesting t
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   587
38692
89d3550d8e16 cosmetics
blanchet
parents: 38689
diff changeset
   588
(* 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
   589
   was 11. *)
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   590
val max_apply_depth = 15
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   591
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   592
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
   593
  | apply_depth (Abs (_, _, t)) = apply_depth t
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   594
  | apply_depth _ = 0
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   595
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   596
fun is_formula_too_complex t =
38085
cc44e887246c avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents: 38027
diff changeset
   597
  apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas [] t
37626
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   598
37543
2e733b0a963c a76ace919f1c wasn't quite right; second try
blanchet
parents: 37538
diff changeset
   599
val exists_sledgehammer_const =
37626
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   600
  exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   601
38904
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   602
(* FIXME: make more reliable *)
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   603
val exists_low_level_class_const =
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   604
  exists_Const (fn (s, _) =>
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   605
     String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s)
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   606
38821
d0275b6c4e9d avoid needless "that" fact
blanchet
parents: 38820
diff changeset
   607
fun is_metastrange_theorem th =
37626
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   608
  case head_of (concl_of th) of
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   609
      Const (a, _) => (a <> @{const_name Trueprop} andalso
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   610
                       a <> @{const_name "=="})
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   611
    | _ => false
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   612
38821
d0275b6c4e9d avoid needless "that" fact
blanchet
parents: 38820
diff changeset
   613
fun is_that_fact th =
d0275b6c4e9d avoid needless "that" fact
blanchet
parents: 38820
diff changeset
   614
  String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th)
d0275b6c4e9d avoid needless "that" fact
blanchet
parents: 38820
diff changeset
   615
  andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
d0275b6c4e9d avoid needless "that" fact
blanchet
parents: 38820
diff changeset
   616
                           | _ => false) (prop_of th)
d0275b6c4e9d avoid needless "that" fact
blanchet
parents: 38820
diff changeset
   617
37626
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   618
val type_has_top_sort =
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   619
  exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37616
diff changeset
   620
38085
cc44e887246c avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents: 38027
diff changeset
   621
(**** 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
   622
      unsoundness) ****)
21470
7c1b59ddcd56 Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents: 21431
diff changeset
   623
38289
74dd8dd33512 adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents: 38279
diff changeset
   624
(* Too general means, positive equality literal with a variable X as one
74dd8dd33512 adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents: 38279
diff changeset
   625
   operand, when X does not occur properly in the other operand. This rules out
74dd8dd33512 adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents: 38279
diff changeset
   626
   clearly inconsistent facts such as X = a | X = b, though it by no means
74dd8dd33512 adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents: 38279
diff changeset
   627
   guarantees soundness. *)
21470
7c1b59ddcd56 Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents: 21431
diff changeset
   628
38289
74dd8dd33512 adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents: 38279
diff changeset
   629
(* Unwanted equalities are those between a (bound or schematic) variable that
74dd8dd33512 adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents: 38279
diff changeset
   630
   does not properly occur in the second operand. *)
38607
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   631
val is_exhaustive_finite =
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   632
  let
38629
3387432c18af more work on finite axiom detection
blanchet
parents: 38627
diff changeset
   633
    fun is_bad_equal (Var z) t =
3387432c18af more work on finite axiom detection
blanchet
parents: 38627
diff changeset
   634
        not (exists_subterm (fn Var z' => z = z' | _ => false) t)
3387432c18af more work on finite axiom detection
blanchet
parents: 38627
diff changeset
   635
      | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j))
3387432c18af more work on finite axiom detection
blanchet
parents: 38627
diff changeset
   636
      | is_bad_equal _ _ = false
3387432c18af more work on finite axiom detection
blanchet
parents: 38627
diff changeset
   637
    fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1
38607
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   638
    fun do_formula pos t =
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   639
      case (pos, t) of
38615
4e1d828ee514 improve "x = A | x = B | x = C"-style axiom detection
blanchet
parents: 38611
diff changeset
   640
        (_, @{const Trueprop} $ t1) => do_formula pos t1
38607
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   641
      | (true, Const (@{const_name all}, _) $ Abs (_, _, t')) =>
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   642
        do_formula pos t'
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   643
      | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) =>
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   644
        do_formula pos t'
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   645
      | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) =>
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   646
        do_formula pos t'
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   647
      | (_, @{const "==>"} $ t1 $ t2) =>
38629
3387432c18af more work on finite axiom detection
blanchet
parents: 38627
diff changeset
   648
        do_formula (not pos) t1 andalso
3387432c18af more work on finite axiom detection
blanchet
parents: 38627
diff changeset
   649
        (t2 = @{prop False} orelse do_formula pos t2)
38786
e46e7a9cb622 formerly unnamed infix impliciation now named HOL.implies
haftmann
parents: 38752
diff changeset
   650
      | (_, @{const HOL.implies} $ t1 $ t2) =>
38629
3387432c18af more work on finite axiom detection
blanchet
parents: 38627
diff changeset
   651
        do_formula (not pos) t1 andalso
3387432c18af more work on finite axiom detection
blanchet
parents: 38627
diff changeset
   652
        (t2 = @{const False} orelse do_formula pos t2)
38607
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   653
      | (_, @{const Not} $ t1) => do_formula (not pos) t1
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   654
      | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   655
      | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38829
diff changeset
   656
      | (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2
38607
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   657
      | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   658
      | _ => false
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   659
  in do_formula true end
a2abe8c2a1c2 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents: 38606
diff changeset
   660
38592
ae6bb801e583 bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq")
blanchet
parents: 38587
diff changeset
   661
fun has_bound_or_var_of_type tycons =
ae6bb801e583 bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq")
blanchet
parents: 38587
diff changeset
   662
  exists_subterm (fn Var (_, Type (s, _)) => member (op =) tycons s
ae6bb801e583 bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq")
blanchet
parents: 38587
diff changeset
   663
                   | Abs (_, Type (s, _), _) => member (op =) tycons s
ae6bb801e583 bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq")
blanchet
parents: 38587
diff changeset
   664
                   | _ => false)
21431
ef9080e7dbbc Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents: 21397
diff changeset
   665
38085
cc44e887246c avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents: 38027
diff changeset
   666
(* Facts are forbidden to contain variables of these types. The typical reason
37347
635425a442e8 show more respect for user-specified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents: 37345
diff changeset
   667
   is that they lead to unsoundness. Note that "unit" satisfies numerous
38085
cc44e887246c avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents: 38027
diff changeset
   668
   equations like "?x = ()". The resulting clauses will have no type constraint,
37347
635425a442e8 show more respect for user-specified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents: 37345
diff changeset
   669
   yielding false proofs. Even "bool" leads to many unsound proofs, though only
635425a442e8 show more respect for user-specified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents: 37345
diff changeset
   670
   for higher-order problems. *)
38592
ae6bb801e583 bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq")
blanchet
parents: 38587
diff changeset
   671
val dangerous_types = [@{type_name unit}, @{type_name bool}, @{type_name prop}];
22217
a5d983f7113f Tidying; more debugging information. New reference unwanted_types.
paulson
parents: 22193
diff changeset
   672
38085
cc44e887246c avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents: 38027
diff changeset
   673
(* Facts containing variables of type "unit" or "bool" or of the form
38290
581a402a80f0 prevent ATP thread for staying around for 1 minute if an exception occurred earlier;
blanchet
parents: 38289
diff changeset
   674
   "ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types
581a402a80f0 prevent ATP thread for staying around for 1 minute if an exception occurred earlier;
blanchet
parents: 38289
diff changeset
   675
   are omitted. *)
38593
85aef7587cf1 minor cleanup
blanchet
parents: 38592
diff changeset
   676
fun is_dangerous_term full_types t =
38609
6220e5ab32f7 more fiddling with Sledgehammer's "add:" option
blanchet
parents: 38607
diff changeset
   677
  not full_types andalso
38679
2cfd0777580f destroy elim rules before checking for finite exhaustive facts
blanchet
parents: 38652
diff changeset
   678
  let val t = transform_elim_term t in
2cfd0777580f destroy elim rules before checking for finite exhaustive facts
blanchet
parents: 38652
diff changeset
   679
    has_bound_or_var_of_type dangerous_types t orelse
2cfd0777580f destroy elim rules before checking for finite exhaustive facts
blanchet
parents: 38652
diff changeset
   680
    is_exhaustive_finite t
2cfd0777580f destroy elim rules before checking for finite exhaustive facts
blanchet
parents: 38652
diff changeset
   681
  end
21470
7c1b59ddcd56 Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents: 21431
diff changeset
   682
38627
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   683
fun is_theorem_bad_for_atps full_types thm =
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   684
  let val t = prop_of thm in
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   685
    is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   686
    is_dangerous_term full_types t orelse exists_sledgehammer_const t orelse
38904
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   687
    exists_low_level_class_const t orelse is_metastrange_theorem thm orelse
5e760c0f81a6 rule out low-level class facts
blanchet
parents: 38901
diff changeset
   688
    is_that_fact thm
38627
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   689
  end
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   690
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
   691
fun clasimpset_rules_of ctxt =
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   692
  let
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   693
    val {safeIs, safeEs, hazIs, hazEs, ...} = ctxt |> claset_of |> rep_cs
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   694
    val intros = safeIs @ hazIs
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   695
    val elims = map Classical.classical_rule (safeEs @ hazEs)
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   696
    val simps = ctxt |> simpset_of |> dest_ss |> #simps |> map snd
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   697
  in (mk_fact_table I intros, mk_fact_table I elims, mk_fact_table I simps) end
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   698
38696
4c6b65d6a135 quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents: 38692
diff changeset
   699
fun all_name_thms_pairs ctxt reserved full_types add_thms chained_ths =
38627
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   700
  let
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   701
    val thy = ProofContext.theory_of ctxt
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   702
    val global_facts = PureThy.facts_of thy
38644
25bbbaf7ce65 don't penalize abstractions in relevance filter + support nameless `foo`-style facts
blanchet
parents: 38629
diff changeset
   703
    val local_facts = ProofContext.facts_of ctxt
25bbbaf7ce65 don't penalize abstractions in relevance filter + support nameless `foo`-style facts
blanchet
parents: 38629
diff changeset
   704
    val named_locals = local_facts |> Facts.dest_static []
38993
504b9e1efd33 give priority to assumptions in structured proofs
blanchet
parents: 38992
diff changeset
   705
    val assms = Assumption.all_assms_of ctxt
504b9e1efd33 give priority to assumptions in structured proofs
blanchet
parents: 38992
diff changeset
   706
    fun is_assum th = exists (fn ct => prop_of th aconv term_of ct) assms
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   707
    val is_chained = member Thm.eq_thm chained_ths
38937
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   708
    val (intros, elims, simps) =
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
   709
      if exists (curry (op <) 0.0) [!intro_bonus, !elim_bonus, !simp_bonus] then
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
   710
        clasimpset_rules_of ctxt
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   711
      else
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   712
        (Termtab.empty, Termtab.empty, Termtab.empty)
38818
61cf050f8b2e improve SPASS hack, when a clause comes from several facts
blanchet
parents: 38816
diff changeset
   713
    (* Unnamed nonchained formulas with schematic variables are omitted, because
61cf050f8b2e improve SPASS hack, when a clause comes from several facts
blanchet
parents: 38816
diff changeset
   714
       they are rejected by the backticks (`...`) parser for some reason. *)
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
   715
    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
   716
      not (Thm.has_name_hint th) andalso
d0f98bd81a85 add nameless chained facts to the pool of things known to Sledgehammer
blanchet
parents: 38819
diff changeset
   717
      (not (exists_subterm is_Var (prop_of th)) orelse (is_chained th)) andalso
38738
0ce517c1970f make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts
blanchet
parents: 38699
diff changeset
   718
      forall (fn (_, ths) => not (member Thm.eq_thm ths th)) named_locals
38644
25bbbaf7ce65 don't penalize abstractions in relevance filter + support nameless `foo`-style facts
blanchet
parents: 38629
diff changeset
   719
    val unnamed_locals =
38820
d0f98bd81a85 add nameless chained facts to the pool of things known to Sledgehammer
blanchet
parents: 38819
diff changeset
   720
      union Thm.eq_thm (Facts.props local_facts) chained_ths
d0f98bd81a85 add nameless chained facts to the pool of things known to Sledgehammer
blanchet
parents: 38819
diff changeset
   721
      |> 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
   722
    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
   723
      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
   724
    fun add_facts global foldx facts =
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   725
      foldx (fn (name0, ths) =>
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   726
        if name0 <> "" andalso
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   727
           forall (not o member Thm.eq_thm add_thms) ths andalso
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   728
           (Facts.is_concealed facts name0 orelse
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   729
            (respect_no_atp andalso is_package_def name0) orelse
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   730
            exists (fn s => String.isSuffix s name0) multi_base_blacklist orelse
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   731
            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
   732
          I
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   733
        else
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   734
          let
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   735
            val multi = length ths > 1
38696
4c6b65d6a135 quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents: 38692
diff changeset
   736
            fun backquotify th =
4c6b65d6a135 quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents: 38692
diff changeset
   737
              "`" ^ Print_Mode.setmp [Print_Mode.input]
4c6b65d6a135 quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents: 38692
diff changeset
   738
                                 (Syntax.string_of_term ctxt) (prop_of th) ^ "`"
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
   739
              |> String.translate (fn c => if Char.isPrint c then str c else "")
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
   740
              |> simplify_spaces
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   741
            fun check_thms a =
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   742
              case try (ProofContext.get_thms ctxt) a of
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   743
                NONE => false
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   744
              | SOME ths' => Thm.eq_thms (ths, ths')
38627
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   745
          in
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   746
            pair 1
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   747
            #> fold (fn th => fn (j, rest) =>
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   748
                 (j + 1,
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   749
                  if is_theorem_bad_for_atps full_types th andalso
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   750
                     not (member Thm.eq_thm add_thms th) then
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   751
                    rest
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   752
                  else
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   753
                    (((fn () =>
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   754
                          if name0 = "" then
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   755
                            th |> backquotify
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   756
                          else
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   757
                            let
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   758
                              val name1 = Facts.extern facts name0
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   759
                              val name2 = Name_Space.extern full_space name0
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   760
                            in
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   761
                              case find_first check_thms [name1, name2, name0] of
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   762
                                SOME name => repair_name reserved multi j name
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   763
                              | NONE => ""
38937
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   764
                            end),
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   765
                      let val t = prop_of th in
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
   766
                        if is_chained th then Chained
38993
504b9e1efd33 give priority to assumptions in structured proofs
blanchet
parents: 38992
diff changeset
   767
                        else if global then
504b9e1efd33 give priority to assumptions in structured proofs
blanchet
parents: 38992
diff changeset
   768
                          if Termtab.defined intros t then Intro
504b9e1efd33 give priority to assumptions in structured proofs
blanchet
parents: 38992
diff changeset
   769
                          else if Termtab.defined elims t then Elim
504b9e1efd33 give priority to assumptions in structured proofs
blanchet
parents: 38992
diff changeset
   770
                          else if Termtab.defined simps t then Simp
504b9e1efd33 give priority to assumptions in structured proofs
blanchet
parents: 38992
diff changeset
   771
                          else General
504b9e1efd33 give priority to assumptions in structured proofs
blanchet
parents: 38992
diff changeset
   772
                        else
504b9e1efd33 give priority to assumptions in structured proofs
blanchet
parents: 38992
diff changeset
   773
                          if is_assum th then Assum else Local
38937
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   774
                      end),
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   775
                      (multi, th)) :: rest)) ths
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   776
            #> snd
38627
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   777
          end)
38644
25bbbaf7ce65 don't penalize abstractions in relevance filter + support nameless `foo`-style facts
blanchet
parents: 38629
diff changeset
   778
  in
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   779
    [] |> add_facts false fold local_facts (unnamed_locals @ named_locals)
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   780
       |> add_facts true Facts.fold_static global_facts global_facts
38644
25bbbaf7ce65 don't penalize abstractions in relevance filter + support nameless `foo`-style facts
blanchet
parents: 38629
diff changeset
   781
  end
38627
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   782
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   783
(* The single-name theorems go after the multiple-name ones, so that single
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   784
   names are preferred when both are available. *)
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   785
fun name_thm_pairs ctxt respect_no_atp =
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   786
  List.partition (fst o snd) #> op @ #> map (apsnd snd)
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   787
  #> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd)
38627
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   788
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   789
(***************************************************************)
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   790
(* ATP invocation methods setup                                *)
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   791
(***************************************************************)
760a2d5cc671 make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents: 38617
diff changeset
   792
38891
6e47e54214b8 remove needless parameter
blanchet
parents: 38889
diff changeset
   793
fun relevant_facts ctxt full_types (threshold0, threshold1) max_relevant
38744
2b6333f78a9e make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents: 38743
diff changeset
   794
                   theory_relevant (relevance_override as {add, del, only})
38891
6e47e54214b8 remove needless parameter
blanchet
parents: 38889
diff changeset
   795
                   chained_ths hyp_ts concl_t =
37538
97ab019d5ac8 make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents: 37537
diff changeset
   796
  let
38822
aa0101e618e2 fix threshold computation + remove "op =" from relevant constants
blanchet
parents: 38821
diff changeset
   797
    val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
aa0101e618e2 fix threshold computation + remove "op =" from relevant constants
blanchet
parents: 38821
diff changeset
   798
                          1.0 / Real.fromInt (max_relevant + 1))
38996
6905ba37376c generalize theorem argument parsing syntax
blanchet
parents: 38994
diff changeset
   799
    val add_thms = Attrib.eval_thms ctxt add
38696
4c6b65d6a135 quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents: 38692
diff changeset
   800
    val reserved = reserved_isar_keyword_table ()
37538
97ab019d5ac8 make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents: 37537
diff changeset
   801
    val axioms =
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   802
      (if only then
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   803
         maps (map (fn ((name, loc), th) => ((K name, loc), (true, th)))
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38751
diff changeset
   804
               o name_thm_pairs_from_ref ctxt reserved chained_ths) add
38699
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   805
       else
27378b4a776b compute names lazily;
blanchet
parents: 38698
diff changeset
   806
         all_name_thms_pairs ctxt reserved full_types add_thms chained_ths)
38688
b2ae937a134b optimize fact filter some more
blanchet
parents: 38687
diff changeset
   807
      |> name_thm_pairs ctxt (respect_no_atp andalso not only)
38937
1b1a2f5ccd7d take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents: 38907
diff changeset
   808
      |> uniquify
37538
97ab019d5ac8 make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents: 37537
diff changeset
   809
  in
38688
b2ae937a134b optimize fact filter some more
blanchet
parents: 38687
diff changeset
   810
    trace_msg (fn () => "Considering " ^ Int.toString (length axioms) ^
b2ae937a134b optimize fact filter some more
blanchet
parents: 38687
diff changeset
   811
                        " theorems");
38745
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   812
    (if threshold0 > 1.0 orelse threshold0 > threshold1 then
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   813
       []
38745
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   814
     else if threshold0 < 0.0 then
38739
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   815
       axioms
8b8ed80b5699 renamed "relevance_convergence" to "relevance_decay"
blanchet
parents: 38738
diff changeset
   816
     else
38745
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   817
       relevance_filter ctxt threshold0 decay max_relevant theory_relevant
ad577fd62ee4 reorganize options regarding to the relevance threshold and decay
blanchet
parents: 38744
diff changeset
   818
                        relevance_override axioms (concl_t :: hyp_ts))
38822
aa0101e618e2 fix threshold computation + remove "op =" from relevant constants
blanchet
parents: 38821
diff changeset
   819
    |> 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
   820
  end
30536
07b4f050e4df split relevance-filter and writing of problem-files;
immler@in.tum.de
parents: 30364
diff changeset
   821
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
   822
end;