src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
changeset 48380 d4b7c7be3116
parent 48308 89674e5a4d35
child 48381 1b7d798460bb
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Jul 20 22:19:45 2012 +0200
     1.3 @@ -0,0 +1,537 @@
     1.4 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
     1.5 +    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     1.6 +    Author:     Jasmin Blanchette, TU Muenchen
     1.7 +
     1.8 +Sledgehammer's iterative relevance filter (MePo = Meng-Paulson).
     1.9 +*)
    1.10 +
    1.11 +signature SLEDGEHAMMER_FILTER_ITER =
    1.12 +sig
    1.13 +  type stature = ATP_Problem_Generate.stature
    1.14 +  type fact = Sledgehammer_Fact.fact
    1.15 +  type params = Sledgehammer_Provers.params
    1.16 +  type relevance_fudge = Sledgehammer_Provers.relevance_fudge
    1.17 +
    1.18 +  val trace : bool Config.T
    1.19 +  val pseudo_abs_name : string
    1.20 +  val pseudo_skolem_prefix : string
    1.21 +  val const_names_in_fact :
    1.22 +    theory -> (string * typ -> term list -> bool * term list) -> term
    1.23 +    -> string list
    1.24 +  val iterative_relevant_facts :
    1.25 +    Proof.context -> params -> string -> int -> relevance_fudge option
    1.26 +    -> term list -> term -> fact list -> fact list
    1.27 +end;
    1.28 +
    1.29 +structure Sledgehammer_Filter_Iter : SLEDGEHAMMER_FILTER_ITER =
    1.30 +struct
    1.31 +
    1.32 +open ATP_Problem_Generate
    1.33 +open Sledgehammer_Fact
    1.34 +open Sledgehammer_Provers
    1.35 +
    1.36 +val trace =
    1.37 +  Attrib.setup_config_bool @{binding sledgehammer_filter_iter_trace} (K false)
    1.38 +fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
    1.39 +
    1.40 +val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
    1.41 +val pseudo_abs_name = sledgehammer_prefix ^ "abs"
    1.42 +val pseudo_skolem_prefix = sledgehammer_prefix ^ "sko"
    1.43 +val theory_const_suffix = Long_Name.separator ^ " 1"
    1.44 +
    1.45 +fun order_of_type (Type (@{type_name fun}, [T1, T2])) =
    1.46 +    Int.max (order_of_type T1 + 1, order_of_type T2)
    1.47 +  | order_of_type (Type (_, Ts)) = fold (Integer.max o order_of_type) Ts 0
    1.48 +  | order_of_type _ = 0
    1.49 +
    1.50 +(* An abstraction of Isabelle types and first-order terms *)
    1.51 +datatype pattern = PVar | PApp of string * pattern list
    1.52 +datatype ptype = PType of int * pattern list
    1.53 +
    1.54 +fun string_for_pattern PVar = "_"
    1.55 +  | string_for_pattern (PApp (s, ps)) =
    1.56 +    if null ps then s else s ^ string_for_patterns ps
    1.57 +and string_for_patterns ps = "(" ^ commas (map string_for_pattern ps) ^ ")"
    1.58 +fun string_for_ptype (PType (_, ps)) = string_for_patterns ps
    1.59 +
    1.60 +(*Is the second type an instance of the first one?*)
    1.61 +fun match_pattern (PVar, _) = true
    1.62 +  | match_pattern (PApp _, PVar) = false
    1.63 +  | match_pattern (PApp (s, ps), PApp (t, qs)) =
    1.64 +    s = t andalso match_patterns (ps, qs)
    1.65 +and match_patterns (_, []) = true
    1.66 +  | match_patterns ([], _) = false
    1.67 +  | match_patterns (p :: ps, q :: qs) =
    1.68 +    match_pattern (p, q) andalso match_patterns (ps, qs)
    1.69 +fun match_ptype (PType (_, ps), PType (_, qs)) = match_patterns (ps, qs)
    1.70 +
    1.71 +(* Is there a unifiable constant? *)
    1.72 +fun pconst_mem f consts (s, ps) =
    1.73 +  exists (curry (match_ptype o f) ps)
    1.74 +         (map snd (filter (curry (op =) s o fst) consts))
    1.75 +fun pconst_hyper_mem f const_tab (s, ps) =
    1.76 +  exists (curry (match_ptype o f) ps) (these (Symtab.lookup const_tab s))
    1.77 +
    1.78 +fun pattern_for_type (Type (s, Ts)) = PApp (s, map pattern_for_type Ts)
    1.79 +  | pattern_for_type (TFree (s, _)) = PApp (s, [])
    1.80 +  | pattern_for_type (TVar _) = PVar
    1.81 +
    1.82 +(* Pairs a constant with the list of its type instantiations. *)
    1.83 +fun ptype thy const x =
    1.84 +  (if const then map pattern_for_type (these (try (Sign.const_typargs thy) x))
    1.85 +   else [])
    1.86 +fun rich_ptype thy const (s, T) =
    1.87 +  PType (order_of_type T, ptype thy const (s, T))
    1.88 +fun rich_pconst thy const (s, T) = (s, rich_ptype thy const (s, T))
    1.89 +
    1.90 +fun string_for_hyper_pconst (s, ps) =
    1.91 +  s ^ "{" ^ commas (map string_for_ptype ps) ^ "}"
    1.92 +
    1.93 +(* Add a pconstant to the table, but a [] entry means a standard
    1.94 +   connective, which we ignore.*)
    1.95 +fun add_pconst_to_table also_skolem (s, p) =
    1.96 +  if (not also_skolem andalso String.isPrefix pseudo_skolem_prefix s) then I
    1.97 +  else Symtab.map_default (s, [p]) (insert (op =) p)
    1.98 +
    1.99 +(* Set constants tend to pull in too many irrelevant facts. We limit the damage
   1.100 +   by treating them more or less as if they were built-in but add their
   1.101 +   axiomatization at the end. *)
   1.102 +val set_consts = [@{const_name Collect}, @{const_name Set.member}]
   1.103 +val set_thms = @{thms Collect_mem_eq mem_Collect_eq Collect_cong}
   1.104 +
   1.105 +fun add_pconsts_in_term thy is_built_in_const also_skolems pos =
   1.106 +  let
   1.107 +    val flip = Option.map not
   1.108 +    (* We include free variables, as well as constants, to handle locales. For
   1.109 +       each quantifiers that must necessarily be skolemized by the automatic
   1.110 +       prover, we introduce a fresh constant to simulate the effect of
   1.111 +       Skolemization. *)
   1.112 +    fun do_const const ext_arg (x as (s, _)) ts =
   1.113 +      let val (built_in, ts) = is_built_in_const x ts in
   1.114 +        if member (op =) set_consts s then
   1.115 +          fold (do_term ext_arg) ts
   1.116 +        else
   1.117 +          (not built_in
   1.118 +           ? add_pconst_to_table also_skolems (rich_pconst thy const x))
   1.119 +          #> fold (do_term false) ts
   1.120 +      end
   1.121 +    and do_term ext_arg t =
   1.122 +      case strip_comb t of
   1.123 +        (Const x, ts) => do_const true ext_arg x ts
   1.124 +      | (Free x, ts) => do_const false ext_arg x ts
   1.125 +      | (Abs (_, T, t'), ts) =>
   1.126 +        ((null ts andalso not ext_arg)
   1.127 +         (* Since lambdas on the right-hand side of equalities are usually
   1.128 +            extensionalized later by "abs_extensionalize_term", we don't
   1.129 +            penalize them here. *)
   1.130 +         ? add_pconst_to_table true (pseudo_abs_name,
   1.131 +                                     PType (order_of_type T + 1, [])))
   1.132 +        #> fold (do_term false) (t' :: ts)
   1.133 +      | (_, ts) => fold (do_term false) ts
   1.134 +    fun do_quantifier will_surely_be_skolemized abs_T body_t =
   1.135 +      do_formula pos body_t
   1.136 +      #> (if also_skolems andalso will_surely_be_skolemized then
   1.137 +            add_pconst_to_table true (pseudo_skolem_prefix ^ serial_string (),
   1.138 +                                      PType (order_of_type abs_T, []))
   1.139 +          else
   1.140 +            I)
   1.141 +    and do_term_or_formula ext_arg T =
   1.142 +      if T = HOLogic.boolT then do_formula NONE else do_term ext_arg
   1.143 +    and do_formula pos t =
   1.144 +      case t of
   1.145 +        Const (@{const_name all}, _) $ Abs (_, T, t') =>
   1.146 +        do_quantifier (pos = SOME false) T t'
   1.147 +      | @{const "==>"} $ t1 $ t2 =>
   1.148 +        do_formula (flip pos) t1 #> do_formula pos t2
   1.149 +      | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
   1.150 +        do_term_or_formula false T t1 #> do_term_or_formula true T t2
   1.151 +      | @{const Trueprop} $ t1 => do_formula pos t1
   1.152 +      | @{const False} => I
   1.153 +      | @{const True} => I
   1.154 +      | @{const Not} $ t1 => do_formula (flip pos) t1
   1.155 +      | Const (@{const_name All}, _) $ Abs (_, T, t') =>
   1.156 +        do_quantifier (pos = SOME false) T t'
   1.157 +      | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
   1.158 +        do_quantifier (pos = SOME true) T t'
   1.159 +      | @{const HOL.conj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
   1.160 +      | @{const HOL.disj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
   1.161 +      | @{const HOL.implies} $ t1 $ t2 =>
   1.162 +        do_formula (flip pos) t1 #> do_formula pos t2
   1.163 +      | Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2 =>
   1.164 +        do_term_or_formula false T t1 #> do_term_or_formula true T t2
   1.165 +      | Const (@{const_name If}, Type (_, [_, Type (_, [T, _])]))
   1.166 +        $ t1 $ t2 $ t3 =>
   1.167 +        do_formula NONE t1 #> fold (do_term_or_formula false T) [t2, t3]
   1.168 +      | Const (@{const_name Ex1}, _) $ Abs (_, T, t') =>
   1.169 +        do_quantifier (is_some pos) T t'
   1.170 +      | Const (@{const_name Ball}, _) $ t1 $ Abs (_, T, t') =>
   1.171 +        do_quantifier (pos = SOME false) T
   1.172 +                      (HOLogic.mk_imp (incr_boundvars 1 t1 $ Bound 0, t'))
   1.173 +      | Const (@{const_name Bex}, _) $ t1 $ Abs (_, T, t') =>
   1.174 +        do_quantifier (pos = SOME true) T
   1.175 +                      (HOLogic.mk_conj (incr_boundvars 1 t1 $ Bound 0, t'))
   1.176 +      | (t0 as Const (_, @{typ bool})) $ t1 =>
   1.177 +        do_term false t0 #> do_formula pos t1  (* theory constant *)
   1.178 +      | _ => do_term false t
   1.179 +  in do_formula pos end
   1.180 +
   1.181 +fun pconsts_in_fact thy is_built_in_const t =
   1.182 +  Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
   1.183 +              (Symtab.empty |> add_pconsts_in_term thy is_built_in_const true
   1.184 +                                                   (SOME true) t) []
   1.185 +
   1.186 +val const_names_in_fact = map fst ooo pconsts_in_fact
   1.187 +
   1.188 +(* Inserts a dummy "constant" referring to the theory name, so that relevance
   1.189 +   takes the given theory into account. *)
   1.190 +fun theory_constify ({theory_const_rel_weight, theory_const_irrel_weight, ...}
   1.191 +                     : relevance_fudge) thy_name t =
   1.192 +  if exists (curry (op <) 0.0) [theory_const_rel_weight,
   1.193 +                                theory_const_irrel_weight] then
   1.194 +    Const (thy_name ^ theory_const_suffix, @{typ bool}) $ t
   1.195 +  else
   1.196 +    t
   1.197 +
   1.198 +fun theory_const_prop_of fudge th =
   1.199 +  theory_constify fudge (Context.theory_name (theory_of_thm th)) (prop_of th)
   1.200 +
   1.201 +fun pair_consts_fact thy is_built_in_const fudge fact =
   1.202 +  case fact |> snd |> theory_const_prop_of fudge
   1.203 +            |> pconsts_in_fact thy is_built_in_const of
   1.204 +    [] => NONE
   1.205 +  | consts => SOME ((fact, consts), NONE)
   1.206 +
   1.207 +(* A two-dimensional symbol table counts frequencies of constants. It's keyed
   1.208 +   first by constant name and second by its list of type instantiations. For the
   1.209 +   latter, we need a linear ordering on "pattern list". *)
   1.210 +
   1.211 +fun pattern_ord p =
   1.212 +  case p of
   1.213 +    (PVar, PVar) => EQUAL
   1.214 +  | (PVar, PApp _) => LESS
   1.215 +  | (PApp _, PVar) => GREATER
   1.216 +  | (PApp q1, PApp q2) =>
   1.217 +    prod_ord fast_string_ord (dict_ord pattern_ord) (q1, q2)
   1.218 +fun ptype_ord (PType p, PType q) =
   1.219 +  prod_ord (dict_ord pattern_ord) int_ord (swap p, swap q)
   1.220 +
   1.221 +structure PType_Tab = Table(type key = ptype val ord = ptype_ord)
   1.222 +
   1.223 +fun count_fact_consts thy fudge =
   1.224 +  let
   1.225 +    fun do_const const (s, T) ts =
   1.226 +      (* Two-dimensional table update. Constant maps to types maps to count. *)
   1.227 +      PType_Tab.map_default (rich_ptype thy const (s, T), 0) (Integer.add 1)
   1.228 +      |> Symtab.map_default (s, PType_Tab.empty)
   1.229 +      #> fold do_term ts
   1.230 +    and do_term t =
   1.231 +      case strip_comb t of
   1.232 +        (Const x, ts) => do_const true x ts
   1.233 +      | (Free x, ts) => do_const false x ts
   1.234 +      | (Abs (_, _, t'), ts) => fold do_term (t' :: ts)
   1.235 +      | (_, ts) => fold do_term ts
   1.236 +  in do_term o theory_const_prop_of fudge o snd end
   1.237 +
   1.238 +fun pow_int _ 0 = 1.0
   1.239 +  | pow_int x 1 = x
   1.240 +  | pow_int x n = if n > 0 then x * pow_int x (n - 1) else pow_int x (n + 1) / x
   1.241 +
   1.242 +(*The frequency of a constant is the sum of those of all instances of its type.*)
   1.243 +fun pconst_freq match const_tab (c, ps) =
   1.244 +  PType_Tab.fold (fn (qs, m) => match (ps, qs) ? Integer.add m)
   1.245 +                 (the (Symtab.lookup const_tab c)) 0
   1.246 +
   1.247 +
   1.248 +(* A surprising number of theorems contain only a few significant constants.
   1.249 +   These include all induction rules, and other general theorems. *)
   1.250 +
   1.251 +(* "log" seems best in practice. A constant function of one ignores the constant
   1.252 +   frequencies. Rare constants give more points if they are relevant than less
   1.253 +   rare ones. *)
   1.254 +fun rel_weight_for _ freq = 1.0 + 2.0 / Math.ln (Real.fromInt freq + 1.0)
   1.255 +
   1.256 +(* Irrelevant constants are treated differently. We associate lower penalties to
   1.257 +   very rare constants and very common ones -- the former because they can't
   1.258 +   lead to the inclusion of too many new facts, and the latter because they are
   1.259 +   so common as to be of little interest. *)
   1.260 +fun irrel_weight_for ({worse_irrel_freq, higher_order_irrel_weight, ...}
   1.261 +                      : relevance_fudge) order freq =
   1.262 +  let val (k, x) = worse_irrel_freq |> `Real.ceil in
   1.263 +    (if freq < k then Math.ln (Real.fromInt (freq + 1)) / Math.ln x
   1.264 +     else rel_weight_for order freq / rel_weight_for order k)
   1.265 +    * pow_int higher_order_irrel_weight (order - 1)
   1.266 +  end
   1.267 +
   1.268 +fun multiplier_for_const_name local_const_multiplier s =
   1.269 +  if String.isSubstring "." s then 1.0 else local_const_multiplier
   1.270 +
   1.271 +(* Computes a constant's weight, as determined by its frequency. *)
   1.272 +fun generic_pconst_weight local_const_multiplier abs_weight skolem_weight
   1.273 +                          theory_const_weight chained_const_weight weight_for f
   1.274 +                          const_tab chained_const_tab (c as (s, PType (m, _))) =
   1.275 +  if s = pseudo_abs_name then
   1.276 +    abs_weight
   1.277 +  else if String.isPrefix pseudo_skolem_prefix s then
   1.278 +    skolem_weight
   1.279 +  else if String.isSuffix theory_const_suffix s then
   1.280 +    theory_const_weight
   1.281 +  else
   1.282 +    multiplier_for_const_name local_const_multiplier s
   1.283 +    * weight_for m (pconst_freq (match_ptype o f) const_tab c)
   1.284 +    |> (if chained_const_weight < 1.0 andalso
   1.285 +           pconst_hyper_mem I chained_const_tab c then
   1.286 +          curry (op *) chained_const_weight
   1.287 +        else
   1.288 +          I)
   1.289 +
   1.290 +fun rel_pconst_weight ({local_const_multiplier, abs_rel_weight,
   1.291 +                        theory_const_rel_weight, ...} : relevance_fudge)
   1.292 +                      const_tab =
   1.293 +  generic_pconst_weight local_const_multiplier abs_rel_weight 0.0
   1.294 +                        theory_const_rel_weight 0.0 rel_weight_for I const_tab
   1.295 +                        Symtab.empty
   1.296 +
   1.297 +fun irrel_pconst_weight (fudge as {local_const_multiplier, abs_irrel_weight,
   1.298 +                                   skolem_irrel_weight,
   1.299 +                                   theory_const_irrel_weight,
   1.300 +                                   chained_const_irrel_weight, ...})
   1.301 +                        const_tab chained_const_tab =
   1.302 +  generic_pconst_weight local_const_multiplier abs_irrel_weight
   1.303 +                        skolem_irrel_weight theory_const_irrel_weight
   1.304 +                        chained_const_irrel_weight (irrel_weight_for fudge) swap
   1.305 +                        const_tab chained_const_tab
   1.306 +
   1.307 +fun stature_bonus ({intro_bonus, ...} : relevance_fudge) (_, Intro) =
   1.308 +    intro_bonus
   1.309 +  | stature_bonus {elim_bonus, ...} (_, Elim) = elim_bonus
   1.310 +  | stature_bonus {simp_bonus, ...} (_, Simp) = simp_bonus
   1.311 +  | stature_bonus {local_bonus, ...} (Local, _) = local_bonus
   1.312 +  | stature_bonus {assum_bonus, ...} (Assum, _) = assum_bonus
   1.313 +  | stature_bonus {chained_bonus, ...} (Chained, _) = chained_bonus
   1.314 +  | stature_bonus _ _ = 0.0
   1.315 +
   1.316 +fun is_odd_const_name s =
   1.317 +  s = pseudo_abs_name orelse String.isPrefix pseudo_skolem_prefix s orelse
   1.318 +  String.isSuffix theory_const_suffix s
   1.319 +
   1.320 +fun fact_weight fudge stature const_tab relevant_consts chained_consts
   1.321 +                fact_consts =
   1.322 +  case fact_consts |> List.partition (pconst_hyper_mem I relevant_consts)
   1.323 +                   ||> filter_out (pconst_hyper_mem swap relevant_consts) of
   1.324 +    ([], _) => 0.0
   1.325 +  | (rel, irrel) =>
   1.326 +    if forall (forall (is_odd_const_name o fst)) [rel, irrel] then
   1.327 +      0.0
   1.328 +    else
   1.329 +      let
   1.330 +        val irrel = irrel |> filter_out (pconst_mem swap rel)
   1.331 +        val rel_weight =
   1.332 +          0.0 |> fold (curry (op +) o rel_pconst_weight fudge const_tab) rel
   1.333 +        val irrel_weight =
   1.334 +          ~ (stature_bonus fudge stature)
   1.335 +          |> fold (curry (op +)
   1.336 +                   o irrel_pconst_weight fudge const_tab chained_consts) irrel
   1.337 +        val res = rel_weight / (rel_weight + irrel_weight)
   1.338 +      in if Real.isFinite res then res else 0.0 end
   1.339 +
   1.340 +fun take_most_relevant ctxt max_facts remaining_max
   1.341 +        ({max_imperfect, max_imperfect_exp, ...} : relevance_fudge)
   1.342 +        (candidates : ((fact * (string * ptype) list) * real) list) =
   1.343 +  let
   1.344 +    val max_imperfect =
   1.345 +      Real.ceil (Math.pow (max_imperfect,
   1.346 +                    Math.pow (Real.fromInt remaining_max
   1.347 +                              / Real.fromInt max_facts, max_imperfect_exp)))
   1.348 +    val (perfect, imperfect) =
   1.349 +      candidates |> sort (Real.compare o swap o pairself snd)
   1.350 +                 |> take_prefix (fn (_, w) => w > 0.99999)
   1.351 +    val ((accepts, more_rejects), rejects) =
   1.352 +      chop max_imperfect imperfect |>> append perfect |>> chop remaining_max
   1.353 +  in
   1.354 +    trace_msg ctxt (fn () =>
   1.355 +        "Actually passed (" ^ string_of_int (length accepts) ^ " of " ^
   1.356 +        string_of_int (length candidates) ^ "): " ^
   1.357 +        (accepts |> map (fn ((((name, _), _), _), weight) =>
   1.358 +                            name () ^ " [" ^ Real.toString weight ^ "]")
   1.359 +                 |> commas));
   1.360 +    (accepts, more_rejects @ rejects)
   1.361 +  end
   1.362 +
   1.363 +fun if_empty_replace_with_scope thy is_built_in_const facts sc tab =
   1.364 +  if Symtab.is_empty tab then
   1.365 +    Symtab.empty
   1.366 +    |> fold (add_pconsts_in_term thy is_built_in_const false (SOME false))
   1.367 +            (map_filter (fn ((_, (sc', _)), th) =>
   1.368 +                            if sc' = sc then SOME (prop_of th) else NONE) facts)
   1.369 +  else
   1.370 +    tab
   1.371 +
   1.372 +fun consider_arities is_built_in_const th =
   1.373 +  let
   1.374 +    fun aux _ _ NONE = NONE
   1.375 +      | aux t args (SOME tab) =
   1.376 +        case t of
   1.377 +          t1 $ t2 => SOME tab |> aux t1 (t2 :: args) |> aux t2 []
   1.378 +        | Const (x as (s, _)) =>
   1.379 +          (if is_built_in_const x args |> fst then
   1.380 +             SOME tab
   1.381 +           else case Symtab.lookup tab s of
   1.382 +             NONE => SOME (Symtab.update (s, length args) tab)
   1.383 +           | SOME n => if n = length args then SOME tab else NONE)
   1.384 +        | _ => SOME tab
   1.385 +  in aux (prop_of th) [] end
   1.386 +
   1.387 +(* FIXME: This is currently only useful for polymorphic type encodings. *)
   1.388 +fun could_benefit_from_ext is_built_in_const facts =
   1.389 +  fold (consider_arities is_built_in_const o snd) facts (SOME Symtab.empty)
   1.390 +  |> is_none
   1.391 +
   1.392 +(* High enough so that it isn't wrongly considered as very relevant (e.g., for E
   1.393 +   weights), but low enough so that it is unlikely to be truncated away if few
   1.394 +   facts are included. *)
   1.395 +val special_fact_index = 75
   1.396 +
   1.397 +fun relevance_filter ctxt thres0 decay max_facts is_built_in_const
   1.398 +        (fudge as {threshold_divisor, ridiculous_threshold, ...}) facts hyp_ts
   1.399 +        concl_t =
   1.400 +  let
   1.401 +    val thy = Proof_Context.theory_of ctxt
   1.402 +    val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty
   1.403 +    val add_pconsts = add_pconsts_in_term thy is_built_in_const false o SOME
   1.404 +    val chained_ts =
   1.405 +      facts |> map_filter (fn ((_, (Chained, _)), th) => SOME (prop_of th)
   1.406 +                            | _ => NONE)
   1.407 +    val chained_const_tab = Symtab.empty |> fold (add_pconsts true) chained_ts
   1.408 +    val goal_const_tab =
   1.409 +      Symtab.empty |> fold (add_pconsts true) hyp_ts
   1.410 +                   |> add_pconsts false concl_t
   1.411 +      |> (fn tab => if Symtab.is_empty tab then chained_const_tab else tab)
   1.412 +      |> fold (if_empty_replace_with_scope thy is_built_in_const facts)
   1.413 +              [Chained, Assum, Local]
   1.414 +    fun iter j remaining_max thres rel_const_tab hopeless hopeful =
   1.415 +      let
   1.416 +        fun relevant [] _ [] =
   1.417 +            (* Nothing has been added this iteration. *)
   1.418 +            if j = 0 andalso thres >= ridiculous_threshold then
   1.419 +              (* First iteration? Try again. *)
   1.420 +              iter 0 max_facts (thres / threshold_divisor) rel_const_tab
   1.421 +                   hopeless hopeful
   1.422 +            else
   1.423 +              []
   1.424 +          | relevant candidates rejects [] =
   1.425 +            let
   1.426 +              val (accepts, more_rejects) =
   1.427 +                take_most_relevant ctxt max_facts remaining_max fudge candidates
   1.428 +              val rel_const_tab' =
   1.429 +                rel_const_tab
   1.430 +                |> fold (add_pconst_to_table false) (maps (snd o fst) accepts)
   1.431 +              fun is_dirty (c, _) =
   1.432 +                Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c
   1.433 +              val (hopeful_rejects, hopeless_rejects) =
   1.434 +                 (rejects @ hopeless, ([], []))
   1.435 +                 |-> fold (fn (ax as (_, consts), old_weight) =>
   1.436 +                              if exists is_dirty consts then
   1.437 +                                apfst (cons (ax, NONE))
   1.438 +                              else
   1.439 +                                apsnd (cons (ax, old_weight)))
   1.440 +                 |>> append (more_rejects
   1.441 +                             |> map (fn (ax as (_, consts), old_weight) =>
   1.442 +                                        (ax, if exists is_dirty consts then NONE
   1.443 +                                             else SOME old_weight)))
   1.444 +              val thres =
   1.445 +                1.0 - (1.0 - thres)
   1.446 +                      * Math.pow (decay, Real.fromInt (length accepts))
   1.447 +              val remaining_max = remaining_max - length accepts
   1.448 +            in
   1.449 +              trace_msg ctxt (fn () => "New or updated constants: " ^
   1.450 +                  commas (rel_const_tab' |> Symtab.dest
   1.451 +                          |> subtract (op =) (rel_const_tab |> Symtab.dest)
   1.452 +                          |> map string_for_hyper_pconst));
   1.453 +              map (fst o fst) accepts @
   1.454 +              (if remaining_max = 0 then
   1.455 +                 []
   1.456 +               else
   1.457 +                 iter (j + 1) remaining_max thres rel_const_tab'
   1.458 +                      hopeless_rejects hopeful_rejects)
   1.459 +            end
   1.460 +          | relevant candidates rejects
   1.461 +                     (((ax as (((_, stature), _), fact_consts)), cached_weight)
   1.462 +                      :: hopeful) =
   1.463 +            let
   1.464 +              val weight =
   1.465 +                case cached_weight of
   1.466 +                  SOME w => w
   1.467 +                | NONE => fact_weight fudge stature const_tab rel_const_tab
   1.468 +                                      chained_const_tab fact_consts
   1.469 +            in
   1.470 +              if weight >= thres then
   1.471 +                relevant ((ax, weight) :: candidates) rejects hopeful
   1.472 +              else
   1.473 +                relevant candidates ((ax, weight) :: rejects) hopeful
   1.474 +            end
   1.475 +        in
   1.476 +          trace_msg ctxt (fn () =>
   1.477 +              "ITERATION " ^ string_of_int j ^ ": current threshold: " ^
   1.478 +              Real.toString thres ^ ", constants: " ^
   1.479 +              commas (rel_const_tab |> Symtab.dest
   1.480 +                      |> filter (curry (op <>) [] o snd)
   1.481 +                      |> map string_for_hyper_pconst));
   1.482 +          relevant [] [] hopeful
   1.483 +        end
   1.484 +    fun uses_const s t =
   1.485 +      fold_aterms (curry (fn (Const (s', _), false) => s' = s | (_, b) => b)) t
   1.486 +                  false
   1.487 +    fun uses_const_anywhere accepts s =
   1.488 +      exists (uses_const s o prop_of o snd) accepts orelse
   1.489 +      exists (uses_const s) (concl_t :: hyp_ts)
   1.490 +    fun add_set_const_thms accepts =
   1.491 +      exists (uses_const_anywhere accepts) set_consts ? append set_thms
   1.492 +    fun insert_into_facts accepts [] = accepts
   1.493 +      | insert_into_facts accepts ths =
   1.494 +        let
   1.495 +          val add = facts |> filter (member Thm.eq_thm_prop ths o snd)
   1.496 +          val (bef, after) =
   1.497 +            accepts |> filter_out (member Thm.eq_thm_prop ths o snd)
   1.498 +                    |> take (max_facts - length add)
   1.499 +                    |> chop special_fact_index
   1.500 +        in bef @ add @ after end
   1.501 +    fun insert_special_facts accepts =
   1.502 +       (* FIXME: get rid of "ext" here once it is treated as a helper *)
   1.503 +       [] |> could_benefit_from_ext is_built_in_const accepts ? cons @{thm ext}
   1.504 +          |> add_set_const_thms accepts
   1.505 +          |> insert_into_facts accepts
   1.506 +  in
   1.507 +    facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)
   1.508 +          |> iter 0 max_facts thres0 goal_const_tab []
   1.509 +          |> insert_special_facts
   1.510 +          |> tap (fn accepts => trace_msg ctxt (fn () =>
   1.511 +                      "Total relevant: " ^ string_of_int (length accepts)))
   1.512 +  end
   1.513 +
   1.514 +fun iterative_relevant_facts ctxt
   1.515 +        ({fact_thresholds = (thres0, thres1), ...} : params) prover
   1.516 +        max_facts fudge hyp_ts concl_t facts =
   1.517 +  let
   1.518 +    val thy = Proof_Context.theory_of ctxt
   1.519 +    val is_built_in_const =
   1.520 +      Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover
   1.521 +    val fudge =
   1.522 +      case fudge of
   1.523 +        SOME fudge => fudge
   1.524 +      | NONE => Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover
   1.525 +    val decay = Math.pow ((1.0 - thres1) / (1.0 - thres0),
   1.526 +                          1.0 / Real.fromInt (max_facts + 1))
   1.527 +  in
   1.528 +    trace_msg ctxt (fn () => "Considering " ^ string_of_int (length facts) ^
   1.529 +                             " facts");
   1.530 +    (if thres1 < 0.0 then
   1.531 +       facts
   1.532 +     else if thres0 > 1.0 orelse thres0 > thres1 then
   1.533 +       []
   1.534 +     else
   1.535 +       relevance_filter ctxt thres0 decay max_facts is_built_in_const fudge
   1.536 +           facts hyp_ts
   1.537 +           (concl_t |> theory_constify fudge (Context.theory_name thy)))
   1.538 +  end
   1.539 +
   1.540 +end;